English
Let f: X → Y be a map between topological spaces and hU an open cover {U_i} of Range f. Then GeneralizingMap f iff for all i, GeneralizingMap ((U_i).carrier.restrictPreimage f).
Русский
Пусть f: X → Y между топологическими пространствами, и hU — открытое покрытие Range f. Тогда GeneralizingMap f эквивалентно тому, что для каждого i отображение, ограниченное до f^{-1}(U_i), является GeneralizingMap.
LaTeX
$$$\operatorname{GeneralizingMap}(f) \iff \forall i,\ \operatorname{GeneralizingMap}\left((U_i).\text{carrier}.\restrictPreimage f\right)$$$
Lean4
theorem generalizingMap_iff_restrictPreimage : GeneralizingMap f ↔ ∀ i, GeneralizingMap ((U i).1.restrictPreimage f) :=
by
refine ⟨fun hf ↦ fun i ↦ hf.restrictPreimage _, fun hf ↦ fun x y h ↦ ?_⟩
obtain ⟨i, hx⟩ := hU.exists_mem (f x)
have h : (⟨y, (U i).2.stableUnderGeneralization h hx⟩ : U i) ⤳ (U i).1.restrictPreimage f ⟨x, hx⟩ := by
rwa [subtype_specializes_iff]
obtain ⟨a, ha, heq⟩ := hf i h
refine ⟨a, ?_, congr(($heq).val)⟩
rwa [subtype_specializes_iff] at ha
