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₁