const_add — Mathlib

English

If f is differentiable on s with continuous derivative, then adding a constant c on the left, i.e., x ↦ c + f(x), preserves differentiability on s.

Русский

Если f дифференцируема на s с непрерывной производной, то слева от f можно добавить константу: x ↦ c + f(x), и дифференцируемость сохраняется на s.

LaTeX

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

Lean4

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

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