English
Continuity of a composition on the left corresponds with continuity of the right function on the corresponding preimage under I.
Русский
Гладкость композиции слева соответствует гладкости правой функции на соответствующем предобразе под I.
LaTeX
$$$ ContinuousWithinAt (f \\circ I^{-1}) (I^{-1}(s) \\cap \\operatorname{range}(I)) (I(x)) \\iff ContinuousWithinAt f s x $$$
Lean4
theorem symm_continuousWithinAt_comp_right_iff {X} [TopologicalSpace X] {f : H → X} {s : Set H} {x : H} :
ContinuousWithinAt (f ∘ I.symm) (I.symm ⁻¹' s ∩ range I) (I x) ↔ ContinuousWithinAt f s x :=
by
refine ⟨fun h => ?_, fun h => ?_⟩
· have := h.comp I.continuousWithinAt (mapsTo_preimage _ _)
simp_rw [preimage_inter, preimage_preimage, I.left_inv, preimage_id', preimage_range, inter_univ] at this
rwa [Function.comp_assoc, I.symm_comp_self] at this
· rw [← I.left_inv x] at h; exact h.comp I.continuousWithinAt_symm inter_subset_left
