Types that are empty #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]
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
- finset.has_emptyc.emptyc.is_empty
- function.embedding.is_empty
- sym.is_empty
- with_top.pred_order.is_empty
- with_bot.succ_order.is_empty
- principal_seg.is_empty
- ordinal.is_empty_out_zero
- weak_dual.character_space.is_empty
- sym2.is_empty
- nonempty_interval.is_empty
- pgame.is_empty_zero_left_moves
- pgame.is_empty_zero_right_moves
- pgame.is_empty_one_right_moves
- pgame.upper_bound_right_moves_empty
- pgame.lower_bound_left_moves_empty
- 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_pow_half_zero_right_moves
- pSet.type.is_empty
- pgame.is_empty_nim_zero_left_moves
- pgame.is_empty_nim_zero_right_moves
- sym_alg.is_empty
- simple_graph.end.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_empty
- first_order.language.is_empty_functions_constants_on_succ
- algebraic_geometry.carrier.is_empty
- algebraic_geometry.Spec_punit_is_empty
- algebraic_geometry.initial_is_empty
@[protected, instance]
subtypes by false are false.
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.
@[protected, instance]