differentiableWithinAt — Mathlib

English

Let b: E × F → G be a bounded bilinear map between normed spaces over 𝕜. Then b is differentiable at every point p ∈ E × F, and hence differentiable on any subset u ⊆ E × F.

Русский

Пусть b: E × F → G — ограниченная билинейная отображение между нормированными пространствами над 𝕜. Тогда b дифференцируема во всех точках p ∈ E × F, а следовательно дифференцируема на любом подмножестве u ⊆ E × F.

LaTeX

$$$\forall p=(p_1,p_2)\in u:\; D b(p) = b(-,p_2) + b(p_1,-) .$$$

Lean4

@[fun_prop]
theorem differentiableWithinAt (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : DifferentiableWithinAt 𝕜 b u p :=
  (h.differentiableAt p).differentiableWithinAt

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