mfderiv_eq_fderiv — Mathlib

English

The mfderivWithin equals fderivWithin for maps between vector spaces.

Русский

Функции mfderivWithin совпадает с fderivWithin для отображений между векторными пространствами.

LaTeX

$$$ mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f s x = fderivWithin 𝕜 f s x $$$

Lean4

/-- For maps between vector spaces, `mfderiv` and `fderiv` coincide -/
@[simp]
theorem mfderiv_eq_fderiv : mfderiv 𝓘(𝕜, E) 𝓘(𝕜, E') f x = fderiv 𝕜 f x :=
  by
  rw [← mfderivWithin_univ, ← fderivWithin_univ]
  exact mfderivWithin_eq_fderivWithin

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