r1Space_iff_inseparable_or_disjoint_nhds

English

A space is R1 if and only if for any x,y, either x,y are inseparable or nhds x and nhds y are disjoint.

Русский

Пространство является R1 тогда и только тогда, когда для любых x,y либо x и y неразделимы, либо nhds x и nhds y неразделимы.

LaTeX

$$$ \\forall X [TopologicalSpace X],\\ Iff( R1Space X, \\forall x y : X, Inseparable x y \\lor Disjoint(\\mathcal{N}_x, \\mathcal{N}_y)). $$$

Lean4

theorem r1Space_iff_inseparable_or_disjoint_nhds {X : Type*} [TopologicalSpace X] :
    R1Space X ↔ ∀ x y : X, Inseparable x y ∨ Disjoint (𝓝 x) (𝓝 y) :=
  ⟨fun _h x y ↦ (specializes_or_disjoint_nhds x y).imp_left Specializes.inseparable, fun h ↦
    ⟨fun x y ↦ (h x y).imp_left Inseparable.specializes⟩⟩

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