isSeparatedMap_iff_disjoint_nhds — Mathlib

English

A map f is separated iff for all x1,x2 with f(x1)=f(x2) and x1≠x2, the neighborhoods nontrivially separate: nhds x1 and nhds x2 are disjoint.

Русский

Карта разделима тогда и только тогда, когда для любых x1≠x2 с f(x1)=f(x2) их нейдш образуют непересекающиеся окрестности.

LaTeX

$$$$\\operatorname{IsSeparatedMap}(f) \\iff \\forall x_1,x_2, f(x_1)=f(x_2) \\to x_1\\neq x_2 \\to \\operatorname{Disjoint}(\\mathcal{N}x_1, \\mathcal{N}x_2).$$$$

Lean4

theorem isSeparatedMap_iff_disjoint_nhds {f : X → Y} :
    IsSeparatedMap f ↔ ∀ x₁ x₂, f x₁ = f x₂ → x₁ ≠ x₂ → Disjoint (𝓝 x₁) (𝓝 x₂) :=
  forall₃_congr fun x x' _ ↦ by
    simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens x'), ← exists_and_left, and_assoc, and_comm,
      and_left_comm]

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