disjoint_nhds_nhds_iff_not_inseparable

English

For points x,y in an R1-space, the neighborhoods nhds x and nhds y are disjoint if and only if x and y are not inseparable.

Русский

Для точек x,y в R1-пространстве окрестности nhds x и nhds y являются взаимно исключающимися тогда и только тогда, когда x и y не несущепредельны (inseparable).

LaTeX

$$$ Disjoint(\\mathcal{N}_x, \\mathcal{N}_y) \\iff \\neg Inseparable(x,y). $$$

Lean4

theorem disjoint_nhds_nhds_iff_not_inseparable : Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y := by
  rw [disjoint_nhds_nhds_iff_not_specializes, specializes_iff_inseparable]

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