English
For any c, s, x, the gauge satisfies ||c|| × egauge 𝕜 s x ≤ egauge 𝕜 s (c • x); i.e., scaling the point x scales the gauge by ||c||.
Русский
Для любого c, s, x верно: ||c|| · egauge 𝕜 s x ≤ egauge 𝕜 s (c • x).
LaTeX
$$$\\forall 𝕜\\,[\\text{NormedDivisionRing } 𝕜],\\; \\forall c\\in 𝕜,\\; \\forall s\\subseteq E,\\; \\forall x:\\; \\|c\\|_{e} \\cdot \\operatorname{egauge}_{\\mathbb{k}}(s,x) \\le \\operatorname{egauge}_{\\mathbb{k}}(s, c\\cdot x).$$$
Lean4
theorem le_egauge_smul_right (c : 𝕜) (s : Set E) (x : E) : ‖c‖ₑ * egauge 𝕜 s x ≤ egauge 𝕜 s (c • x) :=
by
rw [le_egauge_iff]
rintro a ⟨y, hy, hxy⟩
rcases eq_or_ne c 0 with rfl | hc
· simp
· refine ENNReal.mul_le_of_le_div' <| le_trans ?_ ENNReal.coe_div_le
rw [div_eq_inv_mul, ← nnnorm_inv, ← nnnorm_mul]
refine egauge_le_of_mem_smul ⟨y, hy, ?_⟩
simp only [mul_smul, hxy, inv_smul_smul₀ hc]
