Theorems · Theorem · logic and foundations
Set.Nonempty.to_subtype
∀ {α : Type u} {s : Set α}, s.Nonempty → Nonempty ↑s- Defined in
- Mathlib.Data.Set.Basic
- Cited by
- 55 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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 · cited by 7,166
- Set.Nonemptystatement · cited by 2,627
- nonempty_subtypeproof · cited by 22
Cited by55
Results whose statement or proof uses this declaration.
- Set.IsWF.min_memproof · cited by 20
- IsCompact.exists_isLeastproof · cited by 9
- LowerSemicontinuousOn.exists_isMinOnproof · cited by 6
- Submodule.mem_sSup_of_directedproof · cited by 6
- Ordinal.isNormal_derivFamilyproof · cited by 5
- Filter.mem_biInf_of_directedproof · cited by 5
- Ordinal.derivFamily_fpproof · cited by 3
- comap_coe_nhdsLT_eq_atTop_iffproof · cited by 2
- GaloisConnection.l_ciSup_setproof · cited by 2
- Subtype.connectedSpaceproof · cited by 2
- hasBasis_nhdsSet_Iic_Iicproof · cited by 2
- Set.biInter_interproof · cited by 2