lineDifferentiableWithinAt_smul_iff

English

For c ≠ 0, LineDifferentiableAt 𝕜 f x (c • v) is equivalent to LineDifferentiableAt 𝕜 f x v.

Русский

Для c ≠ 0, LineDifferentiableAt 𝕜 f x (c • v) эквивалентно LineDifferentiableAt 𝕜 f x v.

LaTeX

$$$$ (hc : c \neq 0) \Rightarrow LineDifferentiableAt 𝕜 f x (c \cdot v) \iff LineDifferentiableAt 𝕜 f x v $$$$

Lean4

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

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