fderiv_pullback — Mathlib

English

If fderiv 𝕜 f x is invertible, then applying the derivative to the pullback yields V(f x).

Русский

Если fderiv 𝕜 f x обратимо, то производная от pullback 𝕜 f V x равна V(f x).

LaTeX

$$$ fderiv 𝕜 f x (pullback 𝕜 f V x) = V (f x) $$$

Lean4

theorem fderiv_pullback (f : E → F) (V : F → F) (x : E) (h'f : (fderiv 𝕜 f x).IsInvertible) :
    fderiv 𝕜 f x (pullback 𝕜 f V x) = V (f x) :=
  by
  rcases h'f with ⟨M, hM⟩
  simp [pullback_eq_of_fderiv_eq hM, ← hM]

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