instR0SpaceOfPerfectlyNormalSpace

English

In a perfectly normal space, the R0 separation axiom holds; distinct points have distinct neighborhood structures.

Русский

В совершенном нормальном пространстве выполняется ось разделения R0: разные точки имеют разные окрестности.

LaTeX

$$$ \operatorname{PerfectlyNormalSpace}(X) \Rightarrow \operatorname{R0Space}(X) $$$

Lean4

instance (priority := 100) [PerfectlyNormalSpace X] : R0Space X where
  specializes_symmetric x y
    hxy := by
    rw [specializes_iff_forall_closed]
    intro K hK hyK
    apply IsClosed.isGδ at hK
    obtain ⟨Ts, hoTs, -, rfl⟩ := hK
    rw [mem_sInter] at hyK ⊢
    intros
    solve_by_elim [hxy.mem_open]

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