disjoint_lift'_closure_nhds — Mathlib

English

In a T25 space, the lifted closures of the neighborhoods of two distinct points x and y are disjoint if and only if x ≠ y.

Русский

В пространстве T25 замыкания окрестностей двух различных точек x и y, поднятые через lift' closure, непересекаются тогда и только тогда, когда x ≠ y.

LaTeX

$$$\operatorname{Disjoint}\bigl((\mathcal{N}(x))^{\uparrow\text{closure}}, (\mathcal{N}(y))^{\uparrow\text{closure}}\bigr) \iff x \neq y.$$$

Lean4

@[simp]
theorem disjoint_lift'_closure_nhds [T25Space X] {x y : X} :
    Disjoint ((𝓝 x).lift' closure) ((𝓝 y).lift' closure) ↔ x ≠ y :=
  ⟨fun h hxy => by simp [hxy, nhds_neBot.ne] at h, fun h => T25Space.t2_5 h⟩
    -- see Note [lower instance priority]

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