English
If c ≠ 0, then egauge 𝕜 (c • s) x = egauge 𝕜 s x / ||c||.
Русский
Если c ≠ 0, то egauge 𝕜 (c • s) x = egauge 𝕜 s x / ||c||.
LaTeX
$$$\\forall 𝕜\\,[\\text{NormedDivisionRing } 𝕜],\\; \\forall c\\ne 0,\\; \\forall s\\subseteq E,\\; \\forall x:\\; \\operatorname{egauge}_{\\mathbb{k}}(c\\cdot s, x) = \\frac{\\operatorname{egauge}_{\\mathbb{k}}(s,x)}{\\|c\\|_{e}}.$$$
Lean4
theorem egauge_smul_right (h : c = 0 → s.Nonempty) (x : E) : egauge 𝕜 s (c • x) = ‖c‖ₑ * egauge 𝕜 s x :=
by
refine le_antisymm ?_ (le_egauge_smul_right c s x)
rcases eq_or_ne c 0 with rfl | hc
· simp [egauge_zero_right _ (h rfl)]
· rw [mul_comm, ← ENNReal.div_le_iff_le_mul (.inl <| by simpa) (.inl enorm_ne_top), ENNReal.div_eq_inv_mul, ←
enorm_inv (by simpa)]
refine (le_egauge_smul_right _ _ _).trans_eq ?_
rw [inv_smul_smul₀ hc]
