Theorems · Theorem · general topology
Dense.inter_open_nonempty
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).NonemptyAlias of the forward direction of dense_iff_inter_open.
A set is dense if and only if it has a nonempty intersection with each nonempty open set.
- Defined in
- Mathlib.Topology.Closure
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 64 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 · cited by 2,627
- IsOpenstatement · cited by 2,400
- Densestatement · cited by 359
- dense_iff_inter_openproof · cited by 13
Cited by8
Results whose statement or proof uses this declaration.
- Dense.exists_mem_openproof · cited by 10
- Dense.inter_nhds_nonemptyproof · cited by 3
- Dense.nonempty_iffproof · cited by 2
- IsClosed.two_pow_mk_le_two_pow_mk_denseproof · cited by 2
- dense_compl_singleton_iff_not_openproof · cited by 1
- TopologicalSpace.Compacts.separableSpace_iffproof · cited by 1
- not_isMeagre_of_isOpenproof · cited by 0
- IsOpenMap.separableSpace_of_isInducingproof · cited by 0