gauge_gaugeRescale — Mathlib

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'

Похожие утверждения