isClosedEmbedding_iff_restrictPreimage

English

Let f: X → Y be continuous between topological spaces, with {U_i} an open cover of Range(f) by opens. Then f is a closed embedding iff each restricted map f|_{f^{-1}(U_i)} is a closed embedding.

Русский

Пусть f: X → Y непрерывно. Пусть покрытиеRange(f) состоит из открытых множеств. Тогда f является замкнутым вложением тогда и только тогда, когда каждое ограничение f|_{f^{-1}(U_i)} является замкнутым вложением.

LaTeX

$$$\operatorname{IsClosedEmbedding}(f) \iff \forall i, \operatorname{IsClosedEmbedding}\left(f\big|_{f^{-1}(U_i)}\right)$$$

Lean4

theorem isClosedEmbedding_iff_restrictPreimage (h : Continuous f) :
    IsClosedEmbedding f ↔ ∀ i, IsClosedEmbedding ((U i).1.restrictPreimage f) :=
  by
  simp_rw [isClosedEmbedding_iff, forall_and]
  apply and_congr
  · exact hU.isEmbedding_iff_restrictPreimage h
  · simp_rw [range_restrictPreimage]
    exact hU.isClosed_iff_coe_preimage

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