English
There is a natural homeomorphism between the set of functions that coincide with a given family away from S and the product of their restriction to S with the ambient values on S.
Русский
Существует естественная биекция непрерывности между множеством функций, совпадающих с заданной семействой вне S, и произведением их ограничений на S и значений на S.
LaTeX
$$$\\text{There is a homeomorphism }\\operatorname{preimageImageRestrict}(\\alpha,S,s):\\; S^{c}.\\restrict^{-1}'(S^{c}.\\restrict '' s) \\cong_{t} S^{c}.\\restrict '' s \\times (\\Pi i\\in S, \\alpha_i).$$$
Lean4
/-- Homeomorphism between the set of functions that coincide with a given set of functions away
from a given set `S`, and dependent functions away from `S` times any value on `S`. -/
noncomputable def _root_.Homeomorph.preimageImageRestrict (α : ι → Type*) [∀ i, TopologicalSpace (α i)] (S : Set ι)
(s : Set (Π j, α j)) : Sᶜ.restrict ⁻¹' (Sᶜ.restrict '' s) ≃ₜ Sᶜ.restrict '' s × (Π i : S, α i)
where
toFun x := ⟨⟨Sᶜ.restrict x, x.2⟩, fun i ↦ (x : Π j, α j) i⟩
invFun p := ⟨reorderRestrictProd S s p, reorderRestrictProd_mem_preimage_image_restrict p⟩
left_inv x := by ext; simp
right_inv p := by ext <;> simp
continuous_toFun := by
refine Continuous.prodMk ?_ ?_
· exact ((Pi.continuous_restrict _).comp continuous_subtype_val).subtype_mk _
· rw [continuous_pi_iff]
exact fun _ ↦ (continuous_apply _).comp continuous_subtype_val
continuous_invFun := continuous_reorderRestrictProd.subtype_mk _
