Types that are empty #
In this file we define a typeclass is_empty
, which expresses that a type has no elements.
Main declaration #
is_empty
: a typeclass that expresses that a type is empty.
@[class]
- false : α → false
is_empty α
expresses that α
is empty.
Instances of this typeclass
- empty.is_empty
- pempty.is_empty
- false.is_empty
- fin.is_empty
- pi.is_empty
- pprod.is_empty_left
- pprod.is_empty_right
- prod.is_empty_left
- prod.is_empty_right
- psum.is_empty
- sum.is_empty
- subtype.is_empty
- subtype.is_empty_false
- sigma.is_empty_left
- mul_opposite.is_empty
- add_opposite.is_empty
- set.has_emptyc.emptyc.is_empty
- plift.is_empty
- ulift.is_empty
- sym.is_empty
- function.embedding.is_empty
- with_top.pred_order.is_empty
- with_bot.succ_order.is_empty
- principal_seg.is_empty
- ordinal.is_empty_out_zero
- algebraic_geometry.carrier.is_empty
- algebraic_geometry.Spec_punit_is_empty
- algebraic_geometry.initial_is_empty
- sym_alg.is_empty
- sym2.is_empty
- W_type.is_empty
- first_order.sequence₂.is_empty
- first_order.language.functions.is_empty
- first_order.language.relations.is_empty
- first_order.language.is_empty_functions_constants_on_succ
- pgame.is_empty_zero_left_moves
- pgame.is_empty_zero_right_moves
- pgame.is_empty_one_right_moves
- pgame.is_empty_left_moves_add
- pgame.is_empty_right_moves_add
- pgame.is_empty_nat_right_moves
- pgame.is_empty_mul_zero_left_moves
- pgame.is_empty_mul_zero_right_moves
- pgame.is_empty_zero_mul_left_moves
- pgame.is_empty_zero_mul_right_moves
- pgame.inv_ty.is_empty
- ordinal.is_empty_zero_to_pgame_left_moves
- ordinal.is_empty_to_pgame_right_moves
- pgame.is_empty_nim_zero_left_moves
- pgame.is_empty_nim_zero_right_moves
- pgame.is_empty_pow_half_zero_right_moves
- pSet.type.is_empty
@[protected]
@[protected, instance]
def
pi.is_empty
{α : Sort u_1}
{p : α → Sort u_2}
[h : nonempty α]
[∀ (x : α), is_empty (p x)] :
is_empty (Π (x : α), p x)
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
subtypes of an empty type are empty
subtypes by an all-false predicate are false.
@[protected, instance]
subtypes by false are false.
@[protected, instance]
Eliminate out of a type that is_empty
(without using projection notation).
Equations
- is_empty_elim a = _.elim
@[protected]
Eliminate out of a type that is_empty
(using projection notation).
Equations
- h.elim a = is_empty_elim a
@[protected]
Non-dependent version of is_empty.elim
. Helpful if the elaborator cannot elaborate h.elim a
correctly.
@[simp]
@[simp]
@[protected, instance]
@[simp]
theorem
function.extend_of_empty
{α : Sort u_1}
{β : Sort u_2}
{γ : Sort u_3}
[is_empty α]
(f : α → β)
(g : α → γ)
(h : β → γ) :
function.extend f g h = h