English
If f and f1 agree on s, then tangentMapWithin I I' f s p = tangentMapWithin I I' f1 s p for p with p.proj ∈ s.
Русский
Если f и f1 совпадают на s, то tangentMapWithin совпадает на p.proj ∈ s.
LaTeX
$$$\\forall p\\in \\text{TangentBundle},\\; p.1\\in s \\Rightarrow tangentMapWithin I I' f s p = tangentMapWithin I I' f_1 s p$$$
Lean4
theorem comp (hg : MDifferentiableWithinAt I' I'' g u (f x)) (hf : MDifferentiableWithinAt I I' f s x)
(h : s ⊆ f ⁻¹' u) : MDifferentiableWithinAt I I'' (g ∘ f) s x :=
by
rcases hf.2 with ⟨f', hf'⟩
have F : HasMFDerivWithinAt I I' f s x f' := ⟨hf.1, hf'⟩
rcases hg.2 with ⟨g', hg'⟩
have G : HasMFDerivWithinAt I' I'' g u (f x) g' := ⟨hg.1, hg'⟩
exact (HasMFDerivWithinAt.comp x G F h).mdifferentiableWithinAt
