Theorems · Definition · general topology
TopologicalSpace.IsOpen
{X : Type u} → [self : TopologicalSpace X] → Set X → PropA predicate saying that a set is an open set. Use IsOpen in the root namespace instead.
- Defined in
- Mathlib.Topology.Defs.Basic
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
Cited by36
Results whose statement or proof uses this declaration.
- IsOpenproof · cited by 2,400
- DiffeologicalSpace.extproof · cited by 4
- TopCat.isOpen_iff_of_isColimitproof · cited by 4
- borel_eq_generateFrom_of_subbasisproof · cited by 2
- Topology.IsScottHausdorff.isOpen_iffproof · cited by 2
- DiffeologicalSpace.CorePlotsOn.mk.injstatement and proof · cited by 1
- DiffeologicalSpace.CorePlotsOn.mk.noConfusionstatement and proof · cited by 1
- AddGroupTopology.ext'statement and proof · cited by 1
- isOpen_foldstatement · cited by 1
- DiffeologicalSpace.casesOnstatement and proof · cited by 1
- DiffeologicalSpace.isOpen_iff_preimages_plotsstatement · cited by 1
- TopologicalSpace.isOpen_interstatement · cited by 1