Theorems · Definition
IsEmpty.elim
{α : Sort u} → IsEmpty α → {p : α → Sort v} → (a : α) → p aEliminate out of a type that IsEmpty (using projection notation).
- Defined in
- Mathlib.Logic.IsEmpty.Defs
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsEmptystatement and proof · cited by 759
- isEmptyElimproof · cited by 59
Cited by47
Results whose statement or proof uses this declaration.
- not_nonempty_iffproof · cited by 20
- Fintype.card_le_one_iffproof · cited by 4
- MultilinearMap.exists_bound_of_continuousproof · cited by 2
- RelEmbedding.acc_iff_isEmpty_subtype_mem_rangeproof · cited by 2
- CategoryTheory.Presieve.preservesProduct_of_isSheafForstatement and proof · cited by 2
- ciSup_partialSups_eqproof · cited by 2
- Profinite.exists_locallyConstantproof · cited by 2
- AlgebraicGeometry.Scheme.bot_mem_precoverageproof · cited by 2
- TensorProduct.exists_sum_tmul_eqproof · cited by 2
- Function.Surjective.of_isEmptyproof · cited by 2
- IsLocallyConstant.exists_eq_constproof · cited by 1
- LieAlgebra.IsKilling.rootSpace_two_smulproof · cited by 1