sub_const — Mathlib

English

If hf is differentiable within s at x, then hf.sub_const c is differentiable within s at x, i.e., f(y) − c is differentiable within s at x.

Русский

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

LaTeX

$$$ (DifferentiableWithinAt 𝕜 f s x) \\Rightarrow DifferentiableWithinAt 𝕜 (\\lambda y, f(y) - c) s x $$$

Lean4

@[fun_prop]
theorem sub_const (hf : DifferentiableWithinAt 𝕜 f s x) (c : F) : DifferentiableWithinAt 𝕜 (fun y => f y - c) s x :=
  (hf.hasFDerivWithinAt.sub_const c).differentiableWithinAt

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