English
There is an equivalence of the ambient space given by gaugeRescale s t, with inverse gaugeRescale t s.
Русский
Существует гомоморфизм эквивалентности пространства, заданный gaugeRescale s t, с обратным gaugeRescale t s.
LaTeX
$$$\\text{gaugeRescale}(s,t) : E \\to E \\text{ is a bijection with inverse } \\text{gaugeRescale}(t,s)$$$
Lean4
theorem gauge_gaugeRescale (s : Set E) {t : Set E} (hta : Absorbent ℝ t) (htb : IsVonNBounded ℝ t) (x : E) :
gauge t (gaugeRescale s t x) = gauge s x :=
by
rcases eq_or_ne x 0 with rfl | hx
· simp
· exact gauge_gaugeRescale' s ((gauge_pos hta htb).2 hx).ne'