Theorems · Theorem · general topology
Dense.exists_mem_open
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Dense s → ∀ {U : Set X}, IsOpen U → U.Nonempty → ∃ x ∈ s, x ∈ U- Defined in
- Mathlib.Topology.Closure
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 65 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
- Dense.inter_open_nonemptyproof · cited by 8
Cited by10
Results whose statement or proof uses this declaration.
- DenseRange.exists_mem_openproof · cited by 6
- Dense.exists_betweenproof · cited by 5
- Dense.exists_le'proof · cited by 4
- Dense.borel_eq_generateFrom_Ico_mem_auxproof · cited by 3
- Dense.exists_ge'proof · cited by 2
- Dense.borel_eq_generateFrom_Icc_mem_auxproof · cited by 2
- Dense.exists_gtproof · cited by 2
- Dense.exists_dist_ltproof · cited by 1
- Dense.exists_ltproof · cited by 1
- Pairwise.countable_of_isOpen_disjointproof · cited by 1