congr_mfderiv — Mathlib

English

If a function f has MF-derivative f' at x, and f' equals f1', then f has MF-derivative f1' at x as well.

Русский

Если функция f имеет MF-дериватив f' в точке x, и f' совпадает с f1', то в той же точке x функция f имеет MF-дериватив f1'.

LaTeX

$$$HasMFDerivAt\ I I'\ f\ x\ f' \land f' = f_1' \Rightarrow HasMFDerivAt\ I I'\ f\ x\ f_1'$$$

Lean4

theorem congr_mfderiv (h : HasMFDerivAt I I' f x f') (h' : f' = f₁') : HasMFDerivAt I I' f x f₁' :=
  h' ▸ h

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