congr_mfderiv — Mathlib

English

If f has MF-derivative within s at x with derivative f' and f' equals f1', then f has MF-derivative within s at x with derivative f1'.

Русский

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

LaTeX

$$$HasMFDerivWithinAt\ I I'\ f\ s\ x\ f' \land f' = f_1' \Rightarrow HasMFDerivWithinAt\ I I'\ f\ s\ x\ f_1'$$$

Lean4

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

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