differentiableAt — Mathlib

English

If a bilinear map h is bounded, then it is differentiable at p; in particular, differentiableAt h p holds.

Русский

Если билинейная карта ограничена, она дифференцируема в p; следовательно, DifferentiableAt h p.

LaTeX

$$$\mathrm{DifferentiableAt}_{\mathbb{K}} h p$$$

Lean4

@[fun_prop]
theorem differentiableAt (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : DifferentiableAt 𝕜 b p :=
  (h.hasFDerivAt p).differentiableAt

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