English
For any nonzero scalar c, the gauge of the scaled set c•s at x is exactly the original gauge divided by ||c||.
Русский
Для не нулевого скаляра c верна равенство: egauge 𝕜 (c•s) x = egauge 𝕜 s x / ||c||.
LaTeX
$$$\\forall 𝕜\\,[\\text{NormedDivisionRing } 𝕜],\\; \\forall c\\neq 0,\\; \\forall s\\subseteq E,\\; \\forall x\\in E:\\; \\operatorname{egauge}_{\\mathbb{k}}(c\\cdot s, x) = \\frac{\\operatorname{egauge}_{\\mathbb{k}}(s, x)}{\\|c\\|_e}. $$$
Lean4
theorem le_egauge_smul_left (c : 𝕜) (s : Set E) (x : E) : egauge 𝕜 s x / ‖c‖ₑ ≤ egauge 𝕜 (c • s) x :=
by
simp_rw [le_egauge_iff, smul_smul]
rintro a ⟨x, hx, rfl⟩
apply ENNReal.div_le_of_le_mul
rw [← enorm_mul]
exact egauge_le_of_mem_smul <| smul_mem_smul_set hx
