lineDifferentiableWithinAt — Mathlib

English

If f is line-differentiable at x in direction v, then it remains line-differentiable within any subset s of the domain, i.e., restricting the domain does not destroy line-differentiability at that point and direction.

Русский

Если функция f линейно дифференцируема в точке x по направлению v, то она остаётся линейно дифференцируемой внутри любого подмножества s области определения в той же точке и направлении.

LaTeX

$$$\\text{LineDifferentiableWithinAt}_{\\mathbb{k}}(f, s, x, v) \\\\text{ follows from } \\text{LineDifferentiableWithinAt}_{\\mathbb{k}}(f, \\mathrm{univ}, x, v) \\\\text{, hence for any } s$,$$

Lean4

theorem lineDifferentiableWithinAt (h : LineDifferentiableAt 𝕜 f x v) : LineDifferentiableWithinAt 𝕜 f s x v :=
  (differentiableWithinAt_univ.2 h).mono (subset_univ _)

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