hasLineDerivWithinAt_smul_iff — Mathlib

English

For any nonzero c, HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v) holds iff HasLineDerivWithinAt 𝕜 f f' s x v holds.

Русский

Для любого ненулевого c условие HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v) эквивалентно HasLineDerivWithinAt 𝕜 f f' s x v.

LaTeX

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

Lean4

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

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