Differentiable — Mathlib

English

If f has compact support, then its derivative has compact support as well.

Русский

Если у f компактная опора, то и её производная имеет компактную опору.

LaTeX

$$$\text{HasCompactSupport } f \Rightarrow \text{HasCompactSupport } (fderiv 𝕜 f)$$$

Lean4

/-- `Differentiable 𝕜 f` means that `f` is differentiable at any point. -/
@[fun_prop]
def Differentiable (f : E → F) :=
  ∀ x, DifferentiableAt 𝕜 f x

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