English
Let f: X → Y be a map between topological spaces and U_i an open cover of Range f. Then IsOpenMap f iff for all i, IsOpenMap (f ∘ incl_i) where incl_i: U_i → X is the inclusion.
Русский
Пусть f: X → Y между топологическими пространствами, U_i — открытое покрытие Range f. Тогда IsOpenMap f эквивалентно тому, что для каждого i отображение f ∘ incl_i является IsOpenMap, где incl_i: U_i → X — включение.
LaTeX
$$$\operatorname{IsOpenMap}(f) \iff \forall i,\ \operatorname{IsOpenMap}\left(f \circ (\iota_i)\right)$$$
Lean4
theorem generalizingMap_iff_comp : GeneralizingMap f ↔ ∀ i, GeneralizingMap (f ∘ ((↑) : U i → α)) :=
by
refine
⟨fun hf ↦ fun i ↦
((U i).isOpenEmbedding'.generalizingMap (U i).isOpenEmbedding'.isOpen_range.stableUnderGeneralization).comp hf,
fun hf ↦ fun x y h ↦ ?_⟩
obtain ⟨i, hi⟩ := hU.exists_mem x
replace h : y ⤳ (f ∘ ((↑) : U i → α)) ⟨x, hi⟩ := h
obtain ⟨a, ha, rfl⟩ := hf i h
use a.val
simp [ha.map (U i).isOpenEmbedding'.continuous]
