differentiableAt_smul_iff — Mathlib

English

For invertible c, differentiability within s is equivalent to differentiability of the scalar-smul by c.

Русский

Для обратимого c дифференцируемость внутри s эквивалентна дифференцируемости после умножения на c.

LaTeX

$$$ \text{DifferentiableWithinAt}_{\mathbb{K}} (c \cdot f) \, s \, x \iff \text{DifferentiableWithinAt}_{\mathbb{K}} f \, s \, x$ при $[Invertible c]$$$

Lean4

/-- If `c` is invertible, `c • f` is differentiable at `x` if and only if `f` is. -/
theorem differentiableAt_smul_iff (c : R) [Invertible c] : DifferentiableAt 𝕜 (c • f) x ↔ DifferentiableAt 𝕜 f x := by
  rw [← differentiableWithinAt_univ, differentiableWithinAt_smul_iff, differentiableWithinAt_univ]

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