derivWithin_sub_const_fun — Mathlib

English

For any c, the derivative within s of the function y ↦ f(y) − c equals the derivative within s of f, i.e. derivWithin (f − c) = derivWithin f.

Русский

Для любого c производная внутри s функции y ↦ f(y) − c равна производной внутри s функции f, то есть derivWithin (f − c) = derivWithin f.

LaTeX

$$$$ \operatorname{derivWithin}(f \; \cdot \; -c) = \operatorname{derivWithin} f. $$$$

Lean4

@[simp]
theorem derivWithin_sub_const_fun (c : F) : derivWithin (f · - c) = derivWithin f :=
  by
  ext
  apply derivWithin_sub_const

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