English
OnePoint X is equipped with a natural topology making the inclusion i: X → OnePoint X a continuous embedding; the open sets are described via preimages and compact complements as in the standard one-point compactification.
Русский
OnePoint X снабжено естественной топологией так, чтобы вложение i: X → OnePoint X было непрерывным вложением; открытые множества описываются через обратные изображения и компакты как в стандартной одноточечной компактфикации.
LaTeX
$$$\\text{TopologicalSpace}(\\mathrm{OnePoint} X)$ с определением открытостей:\\; U \\text{ открыто в } \\mathrm{OnePoint} X \\iff (\\infty \\in U \\to \\operatorname{IsCompact}(i^{-1}(U)^c)) \\wedge \\operatorname{IsOpen}(i^{-1}(U)).$$$
Lean4
instance : TopologicalSpace (OnePoint X)
where
IsOpen s := (∞ ∈ s → IsCompact (((↑) : X → OnePoint X) ⁻¹' s)ᶜ) ∧ IsOpen (((↑) : X → OnePoint X) ⁻¹' s)
isOpen_univ := by simp
isOpen_inter s
t := by
rintro ⟨hms, hs⟩ ⟨hmt, ht⟩
refine ⟨?_, hs.inter ht⟩
rintro ⟨hms', hmt'⟩
simpa [compl_inter] using (hms hms').union (hmt hmt')
isOpen_sUnion S
ho :=
by
suffices IsOpen ((↑) ⁻¹' ⋃₀ S : Set X) by
refine ⟨?_, this⟩
rintro ⟨s, hsS : s ∈ S, hs : ∞ ∈ s⟩
refine IsCompact.of_isClosed_subset ((ho s hsS).1 hs) this.isClosed_compl ?_
exact compl_subset_compl.mpr (preimage_mono <| subset_sUnion_of_mem hsS)
rw [preimage_sUnion]
exact isOpen_biUnion fun s hs => (ho s hs).2
