fderivWithin_pullbackWithin — Mathlib

English

If fderivWithin 𝕜 f s x is invertible, then fderivWithin 𝕜 f s x (pullbackWithin 𝕜 f V s x) = V(f x).

Русский

Если fderivWithin 𝕜 f s x обратимо, то fderivWithin 𝕜 f s x (pullbackWithin 𝕜 f V s x) = V(f x).

LaTeX

$$$ fderivWithin 𝕜 f s x (pullbackWithin 𝕜 f V s x) = V (f x) $$$

Lean4

theorem fderivWithin_pullbackWithin {f : E → F} {V : F → F} {x : E} (h'f : (fderivWithin 𝕜 f s x).IsInvertible) :
    fderivWithin 𝕜 f s x (pullbackWithin 𝕜 f V s x) = V (f x) :=
  by
  rcases h'f with ⟨M, hM⟩
  simp [pullbackWithin_eq_of_fderivWithin_eq hM, ← hM]

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