English
The gauge rescale map is positively homogeneous: for any nonnegative c, gaugeRescale s t (c x) = c · gaugeRescale s t x.
Русский
Положительная однородность: для неотрицательного c выполняется gaugeRescale s t (c x) = c · gaugeRescale s t x.
LaTeX
$$$0 \\le c \\Rightarrow \\operatorname{gaugeRescale}(s,t,c\\cdot x) = c \\cdot \\operatorname{gaugeRescale}(s,t,x)$$$
Lean4
theorem gaugeRescale_smul (s t : Set E) {c : ℝ} (hc : 0 ≤ c) (x : E) :
gaugeRescale s t (c • x) = c • gaugeRescale s t x :=
by
simp only [gaugeRescale, gauge_smul_of_nonneg hc, smul_smul, smul_eq_mul]
rw [mul_div_mul_comm, mul_right_comm, div_self_mul_self]