Theorems · Theorem · general topology
TopologicalSpace.ext
∀ {X : Type u} {f g : TopologicalSpace X}, IsOpen = IsOpen → f = g- Defined in
- Mathlib.Topology.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.univproof · cited by 3,945
- IsOpenstatement and proof · cited by 2,400
- Set.sUnionproof · cited by 392
Cited by15
Results whose statement or proof uses this declaration.
- induced_composeproof · cited by 26
- coinduced_composeproof · cited by 6
- induced_idproof · cited by 4
- DiffeologicalSpace.extproof · cited by 4
- Equiv.induced_symmproof · cited by 3
- coinduced_eq_induced_of_isOpenQuotientMap_of_isInducingproof · cited by 2
- coinduced_idproof · cited by 2
- TopologicalSpace.ext_iffproof · cited by 2
- AddGroupTopology.ext'proof · cited by 1
- GroupTopology.ext'proof · cited by 1
- TopologicalSpace.ext_iff_nhdsproof · cited by 1
- RingTopology.extproof · cited by 1