isSeparatedMap_iff_isClosedEmbedding

English

IsSeparatedMap f is equivalent to the pullback diagonal embedding being a closed embedding.

Русский

Разделяющее отображение f эквивалентно тому, что вложение диагонали вытянутой по f является замкнутым вложением.

LaTeX

$$$\mathrm{IsSeparatedMap}(f) \iff \mathrm{IsClosedEmbedding}(\mathrm{toPullbackDiag}(f))$$$

Lean4

theorem isSeparatedMap_iff_isClosedEmbedding {f : X → Y} : IsSeparatedMap f ↔ IsClosedEmbedding (toPullbackDiag f) :=
  by
  rw [isSeparatedMap_iff_isClosed_diagonal, ← range_toPullbackDiag]
  exact ⟨fun h ↦ ⟨.toPullbackDiag f, h⟩, fun h ↦ h.isClosed_range⟩

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