const_sub — Mathlib

English

If f is differentiable on s with continuous derivative, then the map x ↦ c − f(x) is differentiable on s.

Русский

Если f дифференцируема на s, то c − f(x) дифференцируема на s.

LaTeX

$$$\forall c \in F,\; \text{DiffContOnCl}(\mathit{f}, s) \Rightarrow \text{DiffContOnCl}(\;c - \mathit{f}, s).$$$

Lean4

theorem const_sub (hf : DiffContOnCl 𝕜 f s) (c : F) : DiffContOnCl 𝕜 (fun x => c - f x) s :=
  diffContOnCl_const.sub hf

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