English
Let f: X → Y be continuous between topological spaces. If {U_i} is an open cover of Y by open subsets, then f is inducing if and only if each restricted map f|_{f^{-1}(U_i)}: f^{-1}(U_i) → U_i is inducing.
Русский
Пусть f: X → Y — непрерывное отображение между топологическими пространствами. Пусть {U_i} — открытое покрытие Y совокупностью открытых подмножеств. Тогда f индуцирующее отображение тогда и только тогда, когда каждое ограниченное отображение f|_{f^{-1}(U_i)}: f^{-1}(U_i) → U_i является индуцирующим.
LaTeX
$$$\operatorname{Inducing}(f) \iff \forall i, \operatorname{Inducing}\left(f\big|_{f^{-1}(U_i)}\right)$$$
Lean4
theorem isInducing_iff_restrictPreimage (h : Continuous f) :
IsInducing f ↔ ∀ i, IsInducing ((U i).1.restrictPreimage f) :=
by
simp_rw [← IsInducing.subtypeVal.of_comp_iff, isInducing_iff_nhds, restrictPreimage, MapsTo.coe_restrict, restrict_eq,
← Filter.comap_comap]
constructor
· intro H i x
rw [Function.comp_apply, ← H, ← IsInducing.subtypeVal.nhds_eq_comap]
· intro H x
obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (show f x ∈ iSup U by simp [hU.iSup_eq_top])
simpa [← ((h.1 _ (U i).2).isOpenEmbedding_subtypeVal).map_nhds_eq ⟨x, hi⟩, H i ⟨x, hi⟩, subtype_coe_map_comap] using
preimage_mem_comap ((U i).2.mem_nhds hi)
