fderivWithin_const_smul_of_field — Mathlib

English

For a field, fderivWithin of c · f equals c times fderivWithin f for any c.

Русский

Для поля: fderivWithin (c · f) = c · fderivWithin f для любого c.

LaTeX

$$$ fderivWithin 𝕜 (c \cdot f) \, s \, x = c \cdot fderivWithin 𝕜 f \, s \, x$$$

Lean4

/-- Special case of `fderivWithin_const_smul_of_invertible` over a field: any constant is allowed -/
theorem fderivWithin_const_smul_of_field (c : 𝕜) (hs : UniqueDiffWithinAt 𝕜 s x) :
    fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x :=
  by
  obtain (rfl | ha) := eq_or_ne c 0
  · simp
  · have : Invertible c := invertibleOfNonzero ha
    ext x
    simp [fderivWithin_const_smul_of_invertible c (f := f) hs]

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