fderivWithin — Mathlib

English

For a bounded bilinear map b: E × F → G, the derivative within a set u at p equals the derivative h.deriv p, provided a UniqueDiffWithinAt condition holds.

Русский

Для ограниченной билинейной карты b: E × F → G производная внутри множества u в точке p равна h.deriv p, при условии UniqueDiffWithinAt.

LaTeX

$$$fderivWithin 𝕜 b u p = h.deriv(p)$, with $h$ the derivative data and $UniqueDiffWithinAt 𝕜 u p$.$$

Lean4

protected theorem fderivWithin (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) (hxs : UniqueDiffWithinAt 𝕜 u p) :
    fderivWithin 𝕜 b u p = h.deriv p :=
  by
  rw [DifferentiableAt.fderivWithin (h.differentiableAt p) hxs]
  exact h.fderiv p

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