lineDifferentiableAt — Mathlib

English

If a line-differentiable-within-at holds, and the neighborhood of x is taken, then it induces line-differentiability at x.

Русский

Если имеет место линейная дифференцируемость внутри множества в точке x, и мы рассматриваем окрестность x, это даёт линейную дифференцируемость в точке x.

LaTeX

$$$\text{LineDifferentiableWithinAt}_{\mathbb{k}}(f,s,x,v) \land s \in \mathcal{N}(x) \Rightarrow \text{LineDifferentiableAt}_{\mathbb{k}}(f,x,v)$$$

Lean4

theorem lineDifferentiableAt (h : LineDifferentiableWithinAt 𝕜 f s x v) (hs : s ∈ 𝓝 x) : LineDifferentiableAt 𝕜 f x v :=
  (h.hasLineDerivWithinAt.hasLineDerivAt hs).lineDifferentiableAt

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