pullbackWithin_univ — Mathlib

English

If there is a linear isomorphism M with M = fderivWithin 𝕜 f s x, then pullbackWithin 𝕜 f V s x = M^{-1}(V(f x)).

Русский

Если существует изоморфизм M such that 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)) $$$

Lean4

@[simp]
theorem pullbackWithin_univ {f : E → F} {V : F → F} : pullbackWithin 𝕜 f V univ = pullback 𝕜 f V :=
  by
  ext x
  simp [pullbackWithin, pullback]

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