exists_open_nhds_disjoint_closure

English

In a T25 space, for distinct x,y there exist open sets u containing x and v containing y such that Disjoint(closure(u), closure(v)).

Русский

В пространстве T25 существуют открытые окрестности u и v вокруг x и y соответственно, такие что closure(u) и closure(v) дистинктны.

LaTeX

$$$\exists u,v:\; x\in u,\ y\in v,\ IsOpen(u) \land IsOpen(v) \land Disjoint(\overline{u}, \overline{v}).$$$

Lean4

theorem exists_open_nhds_disjoint_closure [T25Space X] {x y : X} (h : x ≠ y) :
    ∃ u : Set X, x ∈ u ∧ IsOpen u ∧ ∃ v : Set X, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v) := by
  simpa only [exists_prop, and_assoc] using
    ((nhds_basis_opens x).lift'_closure.disjoint_iff (nhds_basis_opens y).lift'_closure).1
      (disjoint_lift'_closure_nhds.2 h)

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