t2_separation — Mathlib

English

Two distinct points can be separated by disjoint open neighborhoods.

Русский

Две разные точки можно отделить непересекающимися открытыми окрестностями.

LaTeX

$$$ [\text{T2Space}(X)] \Rightarrow \forall x \neq y, \exists U,V:\ IsOpen(U) \land IsOpen(V) \land x\in U \land y\in V \land Disjoint(U,V) $$$

Lean4

/-- Two different points can be separated by open sets. -/
theorem t2_separation [T2Space X] {x y : X} (h : x ≠ y) :
    ∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v :=
  T2Space.t2 h

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