isOpenEmbedding_iff_restrictPreimage

English

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

Русский

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

LaTeX

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

Lean4

theorem isOpenEmbedding_iff_restrictPreimage (h : Continuous f) :
    IsOpenEmbedding f ↔ ∀ i, IsOpenEmbedding ((U i).1.restrictPreimage f) :=
  by
  simp_rw [isOpenEmbedding_iff, forall_and]
  apply and_congr
  · exact hU.isEmbedding_iff_restrictPreimage h
  · simp_rw [range_restrictPreimage]
    exact hU.isOpen_iff_coe_preimage

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