eq — Mathlib · SciLib

English

If s has unique differentiability at x, then two HasFDerivWithinAt at x coincide in derivative if they agree in the interior.

Русский

Если для множества s существует уникальная дифференцируемость в x, то два производных совпадают на x, если они согласованы на внутренности.

LaTeX

$$$$ H\text{ UniqueDiffOn}_𝕜 s \rightarrow x\in s \rightarrow HasFDerivWithinAt f f' s x \rightarrow HasFDerivWithinAt f f₁' s x \rightarrow f' = f₁' $$$$

Lean4

theorem eq (H : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (h : HasFDerivWithinAt f f' s x) (h₁ : HasFDerivWithinAt f f₁' s x) :
    f' = f₁' :=
  (H x hx).eq h h₁

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