English
Analogous composition formula on the right: mpullbackWithin I I'' (g ∘ f) V s x = mpullbackWithin I I' f (mpullbackWithin I' I'' g V t) s x.
Русский
Аналогичная формула композиции справа: mpullbackWithin I I'' (g ∘ f) V s x = mpullbackWithin I I' f (mpullbackWithin I' I'' g V t) s x.
LaTeX
$$$$ \mathrm{mpullbackWithin}\ I I'' (g \circ f)\ V\ s\ x = \mathrm{mpullbackWithin}\ I I' f (\mathrm{mpullbackWithin}\ I' I'' g V t) s x $$$$
Lean4
theorem mpullbackWithin_comp_of_left {g : M' → M''} {f : M → M'} {V : Π (x : M''), TangentSpace I'' x} {s : Set M}
{t : Set M'} {x₀ : M} (hf : MDifferentiableWithinAt I I' f s x₀) (h : Set.MapsTo f s t)
(hu : UniqueMDiffWithinAt I s x₀) (hg' : (mfderivWithin I' I'' g t (f x₀)).IsInvertible) :
mpullbackWithin I I'' (g ∘ f) V s x₀ = mpullbackWithin I I' f (mpullbackWithin I' I'' g V t) s x₀ :=
by
simp only [mpullbackWithin]
have hg : MDifferentiableWithinAt I' I'' g t (f x₀) := mdifferentiableWithinAt_of_isInvertible_mfderivWithin hg'
rw [mfderivWithin_comp _ hg hf h hu, Function.comp_apply, IsInvertible.inverse_comp_apply_of_left hg']
