Theorems · Theorem · general topology
dense_iff_inter_open
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).NonemptyA set is dense if and only if it has a nonempty intersection with each nonempty open set.
- Defined in
- Mathlib.Topology.Closure
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 63 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.
Cites6
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
- TopologicalSpacestatement and proof · cited by 24,529
- Set.Nonemptystatement and proof · cited by 2,627
- IsOpenstatement and proof · cited by 2,400
- Densestatement and proof · cited by 359
- mem_closure_iffproof · cited by 15
Cited by13
Results whose statement or proof uses this declaration.
- Dense.inter_open_nonemptyproof · cited by 8
- dense_of_exists_betweenproof · cited by 6
- IsOpen.denseproof · cited by 5
- tendsto_of_no_upcrossingsproof · cited by 2
- AddAction.isTopologicallyTransitive_iff_dense_iUnion_preimageproof · cited by 2
- dense_compl_singleton_iff_not_openproof · cited by 1
- ProfiniteAddGrp.ProfiniteCompletion.denseRangeproof · cited by 1
- TopologicalSpace.Compacts.separableSpace_iffproof · cited by 1
- exists_open_dense_of_open_dense_subtypeproof · cited by 1
- MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersetsproof · cited by 1
- ProfiniteGrp.denseRange_toLimitproof · cited by 1
- ProfiniteGrp.ProfiniteCompletion.denseRangeproof · cited by 1