Theorems · Theorem · logic and foundations
Set.univ_nonempty
∀ {α : Type u} [Nonempty α], Set.univ.Nonempty- Defined in
- Mathlib.Data.Set.Basic
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- Nonempty
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.
- Set.univstatement and proof · cited by 3,945
- Set.Nonemptystatement and proof · cited by 2,627
Cited by22
Results whose statement or proof uses this declaration.
- isConnected_univproof · cited by 9
- IrreducibleSpace.isIrreducible_univproof · cited by 7
- bddBelow_emptyproof · cited by 5
- Function.argminproof · cited by 4
- connectedSpace_iff_univproof · cited by 2
- BoundedContinuousFunction.dist_lt_of_nonempty_compactproof · cited by 2
- exists_idempotent_of_compact_t2_of_continuous_add_leftproof · cited by 2
- exists_idempotent_of_compact_t2_of_continuous_mul_leftproof · cited by 2
- Filter.Tendsto.exists_forall_leproof · cited by 2
- NormedAddCommGroup.exists_norm_nsmul_leproof · cited by 1
- MeasureTheory.measure_unitBall_eq_integral_div_gammaproof · cited by 1
- continuum_le_cardinal_of_nontriviallyNormedFieldproof · cited by 1