instT0Space — Mathlib

English

If X is a T0 space, then OnePoint X is a T0 space as well.

Русский

Если X является пространством T0, то OnePoint X также является пространством T0.

LaTeX

$$$\\text{T0}(X) \\Rightarrow \\text{T0}(\\mathrm{OnePoint}(X)).$$$

Lean4

/-- The one point compactification of a `T0Space` space is a `T0Space`. -/
instance [T0Space X] : T0Space (OnePoint X) :=
  by
  refine ⟨fun x y hxy => ?_⟩
  rcases inseparable_iff.1 hxy with (⟨rfl, rfl⟩ | ⟨x, rfl, y, rfl, h⟩)
  exacts [rfl, congr_arg some h.eq]

Похожие утверждения