English
Let f: X → Y be a map between topological spaces. The map is separated if and only if the pullback diagonal of f is a closed subset of X × X.
Русский
Пусть f: X → Y — отображение между топологическими пространствами. Отображение разделяющее тогда и только тогда, когда диагональ, вытягиваемая по f, является закрытым подмножеством X × X.
LaTeX
$$$\mathrm{IsSeparatedMap}(f) \iff \mathrm{IsClosed}(\mathrm{pullbackDiagonal}(f))$$$
Lean4
theorem isSeparatedMap_iff_isClosed_diagonal {f : X → Y} : IsSeparatedMap f ↔ IsClosed f.pullbackDiagonal :=
by
simp_rw [isSeparatedMap_iff_nhds, ← isOpen_compl_iff, isOpen_iff_mem_nhds, Subtype.forall, Prod.forall, nhds_induced,
nhds_prod_eq]
refine forall₄_congr fun x₁ x₂ _ _ ↦ ⟨fun h ↦ ?_, fun ⟨t, ht, t_sub⟩ ↦ ?_⟩
· simp_rw [← Filter.disjoint_iff, ← compl_diagonal_mem_prod] at h
exact ⟨_, h, subset_rfl⟩
· obtain ⟨s₁, h₁, s₂, h₂, s_sub⟩ := mem_prod_iff.mp ht
exact ⟨s₁, h₁, s₂, h₂, disjoint_left.2 fun x h₁ h₂ ↦ @t_sub ⟨(x, x), rfl⟩ (s_sub ⟨h₁, h₂⟩) rfl⟩
