smul_iff — Mathlib

English

For any nonzero c, UniqueDiffWithinAt 𝕜 (c • s) (c • x) holds iff UniqueDiffWithinAt 𝕜 s x.

Русский

Для ненулевого c выполняется эквивалентность: UniqueDiffWithinAt 𝕜 (c • s) (c • x) ⇔ UniqueDiffWithinAt 𝕜 s x.

LaTeX

$$$$ \\text{UniqueDiffWithinAt } 𝕜 (\\mathrm{instHSMul.hSMul } c\, s) (\\mathrm{instHSMul.hSMul } c\, x) \\iff \\text{UniqueDiffWithinAt } 𝕜 s x $$$$

Lean4

protected theorem smul_iff {c : 𝕜} (hc : c ≠ 0) : UniqueDiffWithinAt 𝕜 (c • s) (c • x) ↔ UniqueDiffWithinAt 𝕜 s x :=
  ⟨fun h ↦ by simpa [hc] using h.smul (inv_ne_zero hc), (.smul · hc)⟩

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