DifferentiableWithinAt — Mathlib

English

A function f is differentiable within a set s at x if there exists a derivative f' such that HasFDerivWithinAt f f' s x holds.

Русский

Функция дифференцируема внутри множества s в точке x, если существует производная f' удовлетворяющая условию HasFDerivWithinAt.

LaTeX

$$$\text{DifferentiableWithinAt } 𝕜 f s x := \exists f' : E \toL[𝕜] F, HasFDerivWithinAt f f' s x$$$

Lean4

/-- A function `f` is differentiable at a point `x` within a set `s` if it admits a derivative
there (possibly non-unique). -/
@[fun_prop]
def DifferentiableWithinAt (f : E → F) (s : Set E) (x : E) :=
  ∃ f' : E →L[𝕜] F, HasFDerivWithinAt f f' s x

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