mfderiv_congr_point — Mathlib

English

If f and f' are equal as functions, then their MF derivatives at any x are equal.

Русский

Если функции f и f' совпадают, то их MF-дифференциалы в любой точке совпадают.

LaTeX

$$$f = f'\\Rightarrow mfderiv I I' f x = mfderiv I I' f' x$$$

Lean4

/-- A congruence lemma for `mfderiv`, (ab)using the fact that `TangentSpace I' (f x)` is
definitionally equal to `E'`. -/
theorem mfderiv_congr_point {x' : M} (h : x = x') : @Eq (E →L[𝕜] E') (mfderiv I I' f x) (mfderiv I I' f x') := by
  subst h; rfl

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