sub_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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