English
The Lie bracket commutes with pullbacks: pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x equals lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x.
Русский
Скобка Ли commuting с вытягиванием: pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x = lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x.
LaTeX
$$$ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x = lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x $$$
Lean4
theorem pullbackWithin {f : E → F} {V : F → F} {s : Set E} {t : Set F} {x : E} (hV : DifferentiableWithinAt 𝕜 V t (f x))
(hf : ContDiffWithinAt 𝕜 2 f s x) (hf' : (fderivWithin 𝕜 f s x).IsInvertible) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s)
(hst : MapsTo f s t) : DifferentiableWithinAt 𝕜 (pullbackWithin 𝕜 f V s) s x :=
by
rcases exists_continuousLinearEquiv_fderivWithin_symm_eq hf hf' hs hx with ⟨M, -, M_symm_smooth, hM, -⟩
simp only [pullbackWithin_eq]
have : DifferentiableWithinAt 𝕜 (fun y ↦ ((M y).symm : F →L[𝕜] E) (V (f y))) s x :=
by
apply DifferentiableWithinAt.clm_apply
· exact M_symm_smooth.differentiableWithinAt le_rfl
· exact hV.comp _ (hf.differentiableWithinAt one_le_two) hst
apply this.congr_of_eventuallyEq
· filter_upwards [hM] with y hy using by simp [← hy]
· have hMx : M x = fderivWithin 𝕜 f s x := by apply mem_of_mem_nhdsWithin hx hM
simp [← hMx]
