English
If two differentiable functions have the same Fréchet derivatives on s, and they agree at a point, then they agree on all of s.
Русский
Если две дифференцируемые функции имеют одинаковые производные Фреше на s и совпадают в одной точке, то они совпадают на всем s.
LaTeX
$$$\text{If } f,g\text{ differentiable on }s\text{ and } f'(x)=g'(x)\text{ for all }x\in s,\text{ and } f(x_0)=g(x_0),\text{ then }f=g\text{ on }s.$$$
Lean4
/-- The set of all tangent directions to the set `s` at the point `x`. -/
def tangentConeAt (s : Set E) (x : E) : Set E :=
{y : E |
∃ (c : ℕ → 𝕜) (d : ℕ → E),
(∀ᶠ n in atTop, x + d n ∈ s) ∧ Tendsto (fun n => ‖c n‖) atTop atTop ∧ Tendsto (fun n => c n • d n) atTop (𝓝 y)}
