hasLineDerivAt_smul_iff — Mathlib

English

For c ≠ 0, HasLineDerivAt 𝕜 f (c • f') x (c • v) holds iff HasLineDerivAt 𝕜 f f' x v holds.

Русский

Для c ≠ 0 условие HasLineDerivAt 𝕜 f (c • f') x (c • v) выполняется тогда и только тогда, когда HasLineDerivAt 𝕜 f f' x v выполняется.

LaTeX

$$$$ (c \neq 0) \Rightarrow HasLineDerivAt 𝕜 f (c \cdot f') x (c \cdot v) \iff HasLineDerivAt 𝕜 f f' x v $$$$

Lean4

theorem hasLineDerivAt_smul_iff {c : 𝕜} (hc : c ≠ 0) :
    HasLineDerivAt 𝕜 f (c • f') x (c • v) ↔ HasLineDerivAt 𝕜 f f' x v :=
  ⟨fun h ↦ by simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c⁻¹), fun h ↦ h.smul c⟩

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