Theorems · Theorem · general topology
isOpen_iff_mem_nhds
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s ↔ ∀ x ∈ s, s ∈ nhds x- Defined in
- Mathlib.Topology.Neighborhoods
- Cited by
- 48 results in Mathlib
- Foundations
- Depth 66 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.
Cites7
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
- Filterstatement · cited by 8,121
- nhdsstatement · cited by 5,554
- IsOpenstatement · cited by 2,400
- Filter.le_principal_iffproof · cited by 87
- isOpen_iff_nhdsproof · cited by 6
Cited by48
Results whose statement or proof uses this declaration.
- continuous_iff_continuousAtproof · cited by 139
- IsOpenMap.of_nhds_leproof · cited by 10
- isOpen_analyticAtproof · cited by 6
- IsOpen.pathComponentInproof · cited by 5
- InnerProductSpace.isOpen_setOfPred_harmonicAtproof · cited by 5
- AddSubgroup.isOpen_of_mem_nhdsproof · cited by 5
- le_of_nhds_le_nhdsproof · cited by 5
- Valued.isClosed_closedBallproof · cited by 4
- isOpen_prod_iffproof · cited by 4
- UniformSpace.hausdorff.isOpen_inter_nonempty_of_isOpenproof · cited by 4
- Valuation.isClosed_closedBallproof · cited by 4
- MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_sdiffproof · cited by 4