differentiableOn — Mathlib

English

If f is a bounded linear map, then f is differentiable on every subset s of E.

Русский

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

LaTeX

$$$$\text{If } h: IsBoundedLinearMap_{\mathbb{K}}(f)\text{, then } \text{DifferentiableOn}_{\mathbb{K}} f\; s.$$$$

Lean4

@[fun_prop]
theorem differentiableOn (h : IsBoundedLinearMap 𝕜 f) : DifferentiableOn 𝕜 f s :=
  h.differentiable.differentiableOn

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