Theorems · Theorem · order theory
Set.subsingleton_coe
∀ {α : Type u} (s : Set α), Subsingleton ↑s ↔ s.Subsingletons, coerced to a type, is a subsingleton type if and only if s is a subsingleton set.
- Defined in
- Mathlib.Data.Set.Subsingleton
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Set.Elemstatement and proof · cited by 7,166
- Set.Subsingletonstatement and proof · cited by 276
- SetCoe.extproof · cited by 9
- SetCoe.ext_iffproof · cited by 4
Cited by12
Results whose statement or proof uses this declaration.
- Set.Subsingleton.coe_sortproof · cited by 3
- IsQuotientCoveringMap.monodromyPerm_injectiveproof · cited by 2
- Finset.card_le_one_iff_subsingleton_coeproof · cited by 2
- SimpleGraph.Subgraph.degree_eq_zero_of_subsingletonproof · cited by 2
- WithBot.denselyOrdered_set_iff_subsingletonproof · cited by 2
- Cardinal.mk_le_one_iff_set_subsingletonproof · cited by 1
- Set.Subsingleton.isDiscreteproof · cited by 1
- IsPreconnected.infinite_of_nontrivialproof · cited by 1
- Set.Subsingleton.denselyOrderedproof · cited by 1
- Cardinal.mk_set_eq_one_iffproof · cited by 1
- Finset.card_le_one_iff_subsingletonproof · cited by 0
- AddAction.mem_fixedPoints_iff_card_orbit_eq_oneproof · cited by 0