isSeparatedMap_iff_isClosedMap — Mathlib

English

IsSeparatedMap f is equivalent to the graph of f being a closed subset of X × Y.

Русский

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

LaTeX

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

Lean4

theorem isSeparatedMap_iff_isClosedMap {f : X → Y} : IsSeparatedMap f ↔ IsClosedMap (toPullbackDiag f) :=
  isSeparatedMap_iff_isClosedEmbedding.trans
    ⟨IsClosedEmbedding.isClosedMap,
      .of_continuous_injective_isClosedMap (IsEmbedding.toPullbackDiag f).continuous (injective_toPullbackDiag f)⟩

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