DifferentiableOn — Mathlib

English

DifferentiableOn 𝕜 f s means that for every x ∈ s, f is differentiable within s at x.

Русский

DifferentiableOn 𝕜 f s означает, что для каждого x ∈ s функция дифференцируема внутри s в точке x.

LaTeX

$$$\text{DifferentiableOn } 𝕜 f s := \forall x \in s, \text{DifferentiableWithinAt } 𝕜 f s x$$$

Lean4

/-- `DifferentiableOn 𝕜 f s` means that `f` is differentiable within `s` at any point of `s`. -/
@[fun_prop]
def DifferentiableOn (f : E → F) (s : Set E) :=
  ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x

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