pullbackWithin_eq — Mathlib

English

If M is a fixed linear isomorphism equal to fderivWithin 𝕜 f s x, then pullbackWithin 𝕜 f V s x equals M^{-1}(V(f x)).

Русский

Если M есть линейное изоморфизм, равный fderivWithin 𝕜 f s x, то pullbackWithin 𝕜 f V s x равно M^{-1}(V(f x)).

LaTeX

$$$ pullbackWithin 𝕜 f V s x = M^{-1} (V (f x)) \quad\text{where } M = fderivWithin 𝕜 f s x $$$

Lean4

theorem pullbackWithin_eq {f : E → F} {V : F → F} {s : Set E} :
    pullbackWithin 𝕜 f V s = fun x ↦ (fderivWithin 𝕜 f s x).inverse (V (f x)) :=
  rfl

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