mfderivWithin_eq_zero — Mathlib

English

If HasMFDerivWithinAt I I' f s x 0, then mfderivWithin I I' f s x = 0.

Русский

Если производная внутри s в x равна нулю, то mfderivWithin f s x = 0.

LaTeX

$$$ (h : HasMFDerivWithinAt I I' f s x 0) : mfderivWithin I I' f s x = 0 $$$

Lean4

theorem mfderivWithin_eq_zero (h : HasMFDerivWithinAt I I' f s x 0) : mfderivWithin I I' f s x = 0 :=
  by
  simp only [mfld_simps, mfderivWithin, h.mdifferentiableWithinAt, ↓reduceIte]
  simp only [HasMFDerivWithinAt, mfld_simps] at h
  rw [fderivWithin, if_pos]
  exact h.2

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