Structures · Topology
CompletelyNormalSpace
A topological space X is a completely normal space provided that for any two sets s, t
such that if both closure s is disjoint with t, and s is disjoint with closure t,
then there exist disjoint neighbourhoods of s and t.
- Defined in
- Mathlib.Topology.Separation.Regular
- Shape
- One type argument · adds completely_normal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances4
- DomMulAct
- DomAddAct
- Subtype
- ULift
How is a type an instance?
Loading the hierarchy index…
Assumed by8
- CompletelyNormalSpace.completely_normal
- Topology.IsInducing.completelyNormalSpace
- instCompletelyNormalSpaceSubtype
- DomMulAct.instCompletelyNormalSpace
- DomAddAct.instCompletelyNormalSpace
- instT5SpaceSeparationQuotientOfCompletelyNormalSpaceOfR0Space
- CompletelyNormalSpace.toNormalSpace
- ULift.instCompletelyNormalSpace
Ancestors0
No ancestors.