English
If y0 = f(x0) and the derivative is invertible, the pullback mpullback_vectorField_preimage_of_eq is C^m at x0.
Русский
Если y0 = f(x0) и производная обратима, пуллбэк mpullback_vectorField_preimage_of_eq является C^m в точке x0.
LaTeX
$$$\text{If } y_0=f(x_0), \text{ then } mpullback_vectorField_preimage_of_eq \text{ is } C^m \text{ at } x_0.$$$
Lean4
theorem contMDiffWithinAt_mpullbackWithin_extChartAt_symm {V : Π (x : M), TangentSpace I x}
(hV : ContMDiffWithinAt I I.tangent m (fun x ↦ (V x : TangentBundle I M)) s x) (hs : UniqueMDiffOn I s) (hx : x ∈ s)
(hmn : m + 1 ≤ n) :
ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E).tangent m
(fun y ↦ (mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm V (range I) y : TangentBundle 𝓘(𝕜, E) E))
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x x) :=
ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq' hV (contMDiffWithinAt_extChartAt_symm_range_self (n := n) x)
(isInvertible_mfderivWithin_extChartAt_symm (mem_extChartAt_target x)) (by simp [hx])
(UniqueMDiffOn.uniqueMDiffOn_target_inter hs x) hmn
((mapsTo_preimage _ _).mono_left inter_subset_right).preimage_mem_nhdsWithin
(Subset.trans inter_subset_left (extChartAt_target_subset_range x)) (extChartAt_to_inv x)
