English
If g has MF derivative within u at f(x) and f has MF derivative within s at x, then g∘f has MF derivative within s at x with composed derivative.
Русский
Если у g есть MF-дифференциал внутри u в точке f(x), а у f есть MF-дифференциал внутри s в x, то g∘f имеет MF-дифференциал внутри s в x с композицием производных.
LaTeX
$$$HasMFDerivWithinAt I' I'' g\\,u\\,(f x)\\,g' \\land HasMFDerivWithinAt I I' f\\,s\\,x\\,f' \\Rightarrow HasMFDerivWithinAt I I'' (g \\circ f)\\,s\\,x\\,(g'\\circ f')$$$
Lean4
/-- A congruence lemma for `mfderiv`, (ab)using the fact that `TangentSpace I' (f x)` is
definitionally equal to `E'`. -/
theorem mfderiv_congr {f' : M → M'} (h : f = f') : @Eq (E →L[𝕜] E') (mfderiv I I' f x) (mfderiv I I' f' x) := by
subst h; rfl
