English
GaugeRescale satisfies associativity: gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x.
Русский
Гейдж-скейл удовлетворяет ассоциативности: gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x.
LaTeX
$$$\\operatorname{gaugeRescale}(t,u,\\operatorname{gaugeRescale}(s,t,x)) = \\operatorname{gaugeRescale}(s,u,x)$$$
Lean4
theorem gaugeRescale_gaugeRescale {s t u : Set E} (hta : Absorbent ℝ t) (htb : IsVonNBounded ℝ t) (x : E) :
gaugeRescale t u (gaugeRescale s t x) = gaugeRescale s u x :=
by
rcases eq_or_ne x 0 with rfl | hx; · simp
rw [gaugeRescale_def s t x, gaugeRescale_smul, gaugeRescale, gaugeRescale, smul_smul, div_mul_div_cancel₀]
exacts [((gauge_pos hta htb).2 hx).ne', div_nonneg (gauge_nonneg _) (gauge_nonneg _)]
