eq — Mathlib · SciLib

English

If a function has a derivative inside a set at a point, the derivative is uniquely determined by the tangent structure; two derivatives must coincide on the tangent cone.

Русский

Уникальность производной внутри множества: производная определяется касательной конусной структурой.

LaTeX

$$$f' = f₁' \text{ on } \text{tangentCone}(s, x)$$$

Lean4

/-- `UniqueDiffWithinAt` achieves its goal: it implies the uniqueness of the derivative. -/
theorem eq (H : UniqueDiffWithinAt 𝕜 s x) (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt f f₁' s x) :
    f' = f₁' :=
  ContinuousLinearMap.ext_on H.1 (hf.unique_on hg)

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