add_const — Mathlib

English

If a function f is differentiable on a set s with continuous differentiability, then adding a constant vector c to f preserves differentiability on s; the derivative remains unchanged.

Русский

Если функция f дифференцируема на множесте s с непрерывной дифференцируемостью, то прибавление константы c к f сохраняет дифференцируемость на s; производная не изменяется.

LaTeX

$$$\text{If } f: E \to F \text{ is differentiable on } s \text{ with continuous derivative, then for every } c \in F,\; (x \mapsto f(x) + c) \text{ is differentiable on } s.$$$

Lean4

theorem add_const (hf : DiffContOnCl 𝕜 f s) (c : F) : DiffContOnCl 𝕜 (fun x => f x + c) s :=
  hf.add diffContOnCl_const

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