English
Let f: X → Y be a map between topological spaces and U_i an open cover of Range f. Then GeneralizingMap f iff for all i, GeneralizingMap (f ∘ inclusion_i) where inclusion_i: U_i → X is the natural inclusion.
Русский
Пусть f: X → Y между топологическими пространствами, U_i — открытое покрытие Range f. Тогда GeneralizingMap f эквивалентно тому, что для каждого i отображение f ∘ incl_i является GeneralizingMap, где incl_i: U_i → X — естественное включение.
LaTeX
$$$\operatorname{GeneralizingMap}(f) \iff \forall i,\ \operatorname{GeneralizingMap}\left(f \circ (\iota_i)\right)$$$
Lean4
theorem isOpenMap_iff_comp : IsOpenMap f ↔ ∀ i, IsOpenMap (f ∘ ((↑) : U i → α)) :=
by
refine ⟨fun hf ↦ fun i ↦ hf.comp (U i).isOpenEmbedding'.isOpenMap, fun hf ↦ ?_⟩
intro V hV
convert isOpen_iUnion (fun i ↦ hf i _ <| isOpen_induced hV)
simp_rw [Set.image_comp, Set.image_preimage_eq_inter_range, ← Set.image_iUnion, Subtype.range_coe_subtype,
SetLike.setOf_mem_eq, hU.iUnion_inter]
