English
If V₁ and W₁ agree with V and W on s, then mlieBracketWithin I V₁ W₁ s x equals mlieBracketWithin I V W s x.
Русский
Если V₁ совпадает с V и W₁ с W на s, то bracket совпадает.
LaTeX
$$Eq (mlieBracketWithin I V₁ W₁ s x) (mlieBracketWithin I V W s x)$$
Lean4
theorem _root_.MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField
(hV : MDifferentiableWithinAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) s x) :
DifferentiableWithinAt 𝕜 (mpullbackWithin 𝓘(𝕜, E) I (extChartAt I x).symm V (range I))
((extChartAt I x).symm ⁻¹' s ∩ range I) (extChartAt I x x) :=
by
apply MDifferentiableWithinAt.differentiableWithinAt
have :=
MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq hV
(contMDiffWithinAt_extChartAt_symm_range x (mem_extChartAt_target x))
(isInvertible_mfderivWithin_extChartAt_symm (mem_extChartAt_target x)) (mem_range_self _) I.uniqueMDiffOn le_rfl
(extChartAt_to_inv x).symm
rw [inter_comm]
exact
((contMDiff_snd_tangentBundle_modelSpace E 𝓘(𝕜, E)).contMDiffAt.mdifferentiableAt
le_rfl).comp_mdifferentiableWithinAt
_ this
