isOpen_setOf_disjoint_nhds_nhds — Mathlib

English

The set of pairs (p,q) in X × X such that 𝓝 p and 𝓝 q are disjoint is open.

Русский

Множество пар (p,q) в X × X, для которых окрестности 𝓝 p и 𝓝 q не пересекаются, открыто.

LaTeX

$$$ IsOpen \\{ p : X \\times X | Disjoint (\\mathcal{N} p.fst) (\\mathcal{N} p.snd) \\} $$$

Lean4

theorem isOpen_setOf_disjoint_nhds_nhds : IsOpen {p : X × X | Disjoint (𝓝 p.1) (𝓝 p.2)} :=
  by
  simp only [isOpen_iff_mem_nhds, Prod.forall, mem_setOf_eq]
  intro x y h
  obtain ⟨U, hU, V, hV, hd⟩ := ((nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)).mp h
  exact
    mem_nhds_prod_iff'.mpr
      ⟨U, V, hU.2, hU.1, hV.2, hV.1, fun ⟨x', y'⟩ ⟨hx', hy'⟩ =>
        disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩

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