English
The tangent map within the composition equals the tangent map within g applied to the tangent map within f: tangentMapWithin I I'' (g ∘ f) s p = tangentMapWithin I' I'' g u ( tangentMapWithin I I' f s p ).
Русский
Пусть касательное отображение внутри композиции равно касательному отображению внутри g, применённому к касательному отображению внутри f.
LaTeX
$$$\text{tangentMapWithin } I I'' (g \circ f) s p = \text{tangentMapWithin } I' I'' g u (\text{tangentMapWithin } I I' f s p).$$$
Lean4
theorem tangentMapWithin_comp_at (p : TangentBundle I M) (hg : MDifferentiableWithinAt I' I'' g u (f p.1))
(hf : MDifferentiableWithinAt I I' f s p.1) (h : s ⊆ f ⁻¹' u) (hps : UniqueMDiffWithinAt I s p.1) :
tangentMapWithin I I'' (g ∘ f) s p = tangentMapWithin I' I'' g u (tangentMapWithin I I' f s p) :=
by
simp only [tangentMapWithin, mfld_simps]
rw [mfderivWithin_comp p.1 hg hf h hps]
rfl
