Theorems · Definition · order theory
Set.Subsingleton
{α : Type u} → Set α → PropA set s is a Subsingleton if it has at most one element.
- Defined in
- Mathlib.Data.Set.Subsingleton
- Cited by
- 276 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 8 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
Cited by282
Results whose statement or proof uses this declaration.
- Set.subsingleton_singletonstatement · cited by 36
- eVariationOn.subsingletonstatement and proof · cited by 22
- Set.Subsingleton.finitestatement and proof · cited by 20
- Set.subsingleton_emptystatement · cited by 16
- Set.Subsingleton.eq_empty_or_singletonstatement and proof · cited by 16
- Set.Subsingleton.eq_singleton_of_memstatement and proof · cited by 16
- MulAction.IsTrivialBlockproof · cited by 15
- Filter.Subsingletonproof · cited by 15
- IsTotallyDisconnectedproof · cited by 14
- Set.Subsingleton.imagestatement and proof · cited by 14
- Set.not_nontrivial_iffstatement · cited by 13
- Set.Subsingleton.antistatement and proof · cited by 13
Showing the 200 most cited of 282.