def PiBase.OnePoint.toSeparationQuotient {X : Type u} [TopologicalSpace X] : X → SeparationQuotient (OnePoint X)

Equations

• PiBase.OnePoint.toSeparationQuotient x = SeparationQuotient.mk ↑x

theorem PiBase.OnePoint.toSeparationQuotient_wellDefined {X : Type u} [TopologicalSpace X] (x y : X) : Inseparable x y → toSeparationQuotient x = toSeparationQuotient y

def PiBase.OnePoint.ofSeparationQuotient {X : Type u} [TopologicalSpace X] : OnePoint X → OnePoint (SeparationQuotient X)

Equations

• PiBase.OnePoint.ofSeparationQuotient none = OnePoint.infty
• PiBase.OnePoint.ofSeparationQuotient (some x_1) = ↑(SeparationQuotient.mk x_1)

theorem PiBase.OnePoint.continuous_ofSeparationQuotient (X : Type u) [TopologicalSpace X] : Continuous ofSeparationQuotient

theorem PiBase.OnePoint.ofSeparationQuotient_wellDefined {X : Type u} [TopologicalSpace X] (x y : OnePoint X) : Inseparable x y → ofSeparationQuotient x = ofSeparationQuotient y

theorem PiBase.OnePoint.isCompact_preimage {X : Type u} [TopologicalSpace X] {s : Set (OnePoint X)} (hs : IsCompact s) (si : OnePoint.infty ∉ s) : IsCompact (OnePoint.some ⁻¹' s)

theorem PiBase.OnePoint.subset_range_some {X : Type u} [TopologicalSpace X] {s : Set (OnePoint X)} (hs : OnePoint.infty ∉ s) : s ⊆ Set.range OnePoint.some

theorem PiBase.OnePoint.isCompact_of_closed {X : Type u} [TopologicalSpace X] {s : Set (OnePoint X)} (hs : IsClosed s) (hi : OnePoint.infty ∉ s) : IsCompact s

def PiBase.OnePoint.SeparationQuotientHomeomorph (X : Type u) [TopologicalSpace X] : SeparationQuotient (OnePoint X) ≃ₜ OnePoint (SeparationQuotient X)

Equations

• One or more equations did not get rendered due to their size.

instance PiBase.OnePoint.instR0Space {X : Type u} [TopologicalSpace X] [t : R0Space X] : R0Space (OnePoint X)