comp — Mathlib

English

If x and x' are equal, the MF derivative at x equals the MF derivative at x'.

Русский

Если x= x', то MF-дифференциал в x равен MF-дифференциалу в x'.

LaTeX

$$$x = x'\\Rightarrow mfderiv I I' f x = mfderiv I I' f x'$$$

Lean4

/-- The **chain rule for manifolds**. -/
theorem comp (hg : HasMFDerivAt I' I'' g (f x) g') (hf : HasMFDerivAt I I' f x f') :
    HasMFDerivAt I I'' (g ∘ f) x (g'.comp f') :=
  by
  rw [← hasMFDerivWithinAt_univ] at *
  exact HasMFDerivWithinAt.comp x (hg.mono (subset_univ _)) hf subset_preimage_univ

Похожие утверждения