instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space

English

If X is weakly locally compact and T1, then OnePoint X is a normal space.

Русский

Если X — слабее локально компактное и T1-пространство, то OnePoint X — нормальное пространство.

LaTeX

$$$\\text{NormalSpace}(\\mathrm{OnePoint}(X))$ under assumptions.$$

Lean4

/-- The one point compactification of a weakly locally compact R₁ space
is a normal topological space. -/
instance [WeaklyLocallyCompactSpace X] [R1Space X] : NormalSpace (OnePoint X) :=
  by
  suffices R1Space (OnePoint X) by infer_instance
  have key : ∀ z : X, Disjoint (𝓝 (some z)) (𝓝 ∞) := fun z ↦
    by
    rw [nhds_infty_eq, disjoint_sup_right, nhds_coe_eq, coclosedCompact_eq_cocompact, disjoint_map coe_injective, ←
      principal_singleton, disjoint_principal_right, compl_infty]
    exact ⟨disjoint_nhds_cocompact z, range_mem_map⟩
  refine ⟨fun x y ↦ ?_⟩
  induction x using OnePoint.rec <;> induction y using OnePoint.rec
  · exact .inl le_rfl
  · exact .inr (key _).symm
  · exact .inr (key _)
  · rw [nhds_coe_eq, nhds_coe_eq, disjoint_map coe_injective, specializes_coe]
    apply specializes_or_disjoint_nhds

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