Theorems · Theorem · general topology
dense_univ
∀ {X : Type u} [inst : TopologicalSpace X], Dense Set.univ- Defined in
- Mathlib.Topology.Closure
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
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.
- TopologicalSpacestatement and proof · cited by 24,529
- Set.univstatement · cited by 3,945
- Densestatement · cited by 359
- subset_closureproof · cited by 309
Cited by12
Results whose statement or proof uses this declaration.
- TopologicalSpace.isSeparable_univ_iffproof · cited by 4
- exists_countable_dense_bot_topproof · cited by 3
- stronglyMeasurable_deriv_with_paramproof · cited by 3
- borel_eq_generateFrom_Icoproof · cited by 2
- exists_countable_dense_no_bot_topproof · cited by 1
- dense_iUnion_interior_of_closedproof · cited by 1
- continuous_prod_of_continuous_lipschitzWithproof · cited by 1
- borel_eq_generateFrom_Iccproof · cited by 1
- Metric.dense_iUnion_range_toInductiveLimitproof · cited by 1
- borel_eq_generateFrom_Iocproof · cited by 1
- dense_sUnion_interior_of_closedproof · cited by 0
- dense_biUnion_interior_of_closedproof · cited by 0