English
For any c, s, x, the gauge satisfies egauge 𝕜 s x / ||c|| ≤ egauge 𝕜 (c • s) x; i.e., scaling the set by c enlarges the gauge by at least the factor 1/||c||.
Русский
Для любого c, s, x верна неравенство: egauge 𝕜 s x / ||c|| ≤ egauge 𝕜 (c·s) x; масштабирование множества на c растягивает шкалу как минимум в 1/||c|| раза.
LaTeX
$$$\\forall 𝕜\\,[\\text{NormedDivisionRing } 𝕜],\\; \\forall c\\in 𝕜,\\; \\forall s\\subseteq E,\\; \\forall x:\\; \\frac{\\operatorname{egauge}_{\\mathbb{k}}(s,x)}{\\|c\\|_{e}} \\le \\operatorname{egauge}_{\\mathbb{k}}(c\\cdot s, x).$$$
Lean4
theorem egauge_smul_left (hc : c ≠ 0) (s : Set E) (x : E) : egauge 𝕜 (c • s) x = egauge 𝕜 s x / ‖c‖ₑ :=
by
refine le_antisymm ?_ (le_egauge_smul_left _ _ _)
rw [ENNReal.le_div_iff_mul_le (by simp [*]) (by simp)]
calc
egauge 𝕜 (c • s) x * ‖c‖ₑ = egauge 𝕜 (c • s) x / ‖c⁻¹‖ₑ := by rw [enorm_inv (by simpa), div_eq_mul_inv, inv_inv]
_ ≤ egauge 𝕜 (c⁻¹ • c • s) x := (le_egauge_smul_left _ _ _)
_ = egauge 𝕜 s x := by rw [inv_smul_smul₀ hc]
