eq_deriv — Mathlib

English

In the presence of UniqueDiffWithinAt, the derivative values are equal if the corresponding HasDerivWithinAt statements hold.

Русский

При наличии UniqueDiffWithinAt производные совпадают при выполнении соответствующих условий.

LaTeX

$$$\\text{UniqueDiffWithinAt}_{\\mathbb{K}}(s,x) \\Rightarrow \\bigl( \\mathrm{HasDerivWithinAt}(f,f',s,x) \\wedge \\mathrm{HasDerivWithinAt}(f,f_1',s,x) \\Rightarrow f' = f_1' \\bigr).$$$

Lean4

theorem eq_deriv (s : Set 𝕜) (H : UniqueDiffWithinAt 𝕜 s x) (h : HasDerivWithinAt f f' s x)
    (h₁ : HasDerivWithinAt f f₁' s x) : f' = f₁' :=
  smulRight_one_eq_iff.mp <| UniqueDiffWithinAt.eq H h h₁

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