Structures · Topology
R0Space
A topological space is called an R₀ space, if Specializes relation is symmetric.
In other words, given two points x y : X,
if every neighborhood of y contains x, then every neighborhood of x contains y.
- Defined in
- Mathlib.Topology.Separation.Basic
- Shape
- One type argument · adds specializes_symm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- DomMulAct
- DomAddAct
- ContinuousMapZero
- Subtype
- Prod
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by23
- specializes_iff_inseparable
- Specializes.symm
- specializes_comm
- Bornology.relativelyCompact
- R0Space.closure_singleton
- Bornology.relativelyCompact.isBounded_iff
- Specializes.inseparable
- R0Space.specializes_symm
- isCompact_closure_singleton
- ContinuousMap.instR0Space
- Topology.IsInducing.r0Space
- instT1SpaceOfT0SpaceOfR0Space
- Filter.coclosedCompact_le_cofinite
- instR0SpaceForall
- ContinuousMapZero.instR0Space
- Set.Finite.isCompact_closure
- instR0SpaceSubtype
- R0Space.specializes_symmetric
- instT5SpaceSeparationQuotientOfCompletelyNormalSpaceOfR0Space
- DomAddAct.instR0Space
- instR0SpaceProd
- DomMulAct.instR0Space
- NormalSpace.instCompletelyRegularSpace
Ancestors0
No ancestors.