exists_nhds_disjoint_closure — Mathlib

English

In a T25 space, for distinct x,y there exist neighborhoods s of x and t of y with Disjoint(closure(s), closure(t)).

Русский

В пространстве T25 для различных x,y существуют окрестности s вокруг x и t вокруг y такие, что closure(s) и closure(t) дизjoint.

LaTeX

$$$\exists s\in \mathcal{N}(x), \exists t\in \mathcal{N}(y),\ Disjoint(\overline{s}, \overline{t}).$$$

Lean4

theorem exists_nhds_disjoint_closure [T25Space X] {x y : X} (h : x ≠ y) :
    ∃ s ∈ 𝓝 x, ∃ t ∈ 𝓝 y, Disjoint (closure s) (closure t) :=
  ((𝓝 x).basis_sets.lift'_closure.disjoint_iff (𝓝 y).basis_sets.lift'_closure).1 <| disjoint_lift'_closure_nhds.2 h

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