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