English
For all c ∈ 𝕜 and x ∈ V, e(c x) = ‖c‖₊ · e(x).
Русский
Для всех c ∈ 𝕜 и x ∈ V выполняется e(c x) = |c|₊ · e(x).
LaTeX
$$e (c • x) = ‖c‖₊ * e x$$
Lean4
@[deprecated "Use ENormedAddCommMonoid or talk to the Carleson project" (since := "2025-05-07"), simp]
theorem map_smul (c : 𝕜) (x : V) : e (c • x) = ‖c‖₊ * e x :=
by
apply le_antisymm (e.map_smul_le' c x)
by_cases hc : c = 0
· simp [hc]
calc
(‖c‖₊ : ℝ≥0∞) * e x = ‖c‖₊ * e (c⁻¹ • c • x) := by rw [inv_smul_smul₀ hc]
_ ≤ ‖c‖₊ * (‖c⁻¹‖₊ * e (c • x)) := (mul_le_mul_left' (e.map_smul_le' _ _) _)
_ = e (c • x) := by
rw [← mul_assoc, nnnorm_inv, ENNReal.coe_inv, ENNReal.mul_inv_cancel _ ENNReal.coe_ne_top, one_mul] <;> simp [hc]