map_smul — Mathlib

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]

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