differentiableAt — Mathlib

English

If f is a bounded linear map, then f is differentiable within any set s at any x, with derivative h.

Русский

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

LaTeX

$$$$ \\text{DifferentiableWithinAt } 𝕜 f s x. $$$$

Lean4

@[fun_prop]
theorem differentiableAt (h : IsBoundedLinearMap 𝕜 f) : DifferentiableAt 𝕜 f x :=
  h.hasFDerivAt.differentiableAt

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