differentiableWithinAt — Mathlib

English

If a linear map e is differentiable, then it is differentiable within any set s and the derivative within s equals e on the interior of s.

Русский

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

LaTeX

$$$$ \\text{DifferentiableWithinAt } 𝕜 e s x \\quad\\Rightarrow\\quad fderivWithin 𝕜 e s x = e. $$$$

Lean4

@[fun_prop]
protected theorem differentiableWithinAt : DifferentiableWithinAt 𝕜 e s x :=
  e.differentiableAt.differentiableWithinAt

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