separatedNhds_iff_disjoint — Mathlib

English

HasSeparatingCover s t means there exists a sequence of open sets whose union covers s and whose closures are disjoint from t.

Русский

HasSeparatingCover s t означает существование последовательности открытых множеств, чья объединение покрывает s, а замкнутые множества каждой u_n не пересекаются с t.

LaTeX

$$$\\exists u : \\mathbb{N} \\to \\mathcal{P}(X),\\ s \\subseteq \\bigcup_n u(n)\\ \\land\\ \\forall n, \\IsOpen(u(n)) \\land \\text{Disjoint}(\\overline{u(n)}, t)$$$

Lean4

theorem separatedNhds_iff_disjoint {s t : Set X} : SeparatedNhds s t ↔ Disjoint (𝓝ˢ s) (𝓝ˢ t) := by
  simp only [(hasBasis_nhdsSet s).disjoint_iff (hasBasis_nhdsSet t), SeparatedNhds, ← exists_and_left, and_assoc,
    and_comm, and_left_comm]

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