English
There is a gaugeRescaleEquiv object providing a bijection with continuous forward and inverse parts between two convex absorbent sets.
Русский
Существует gaugeRescaleEquiv, задающий биекцию между двумя выпуклыми абсорбентными множествами с непрерывной прямой и обратной частями.
LaTeX
$$$\\exists e: E \\simeq E,\\;\\text{gaugeRescaleEquiv}(s,t) = e$ with the stated continuity properties$$
Lean4
/-- `gaugeRescale` bundled as an `Equiv`. -/
def gaugeRescaleEquiv (s t : Set E) (hsa : Absorbent ℝ s) (hsb : IsVonNBounded ℝ s) (hta : Absorbent ℝ t)
(htb : IsVonNBounded ℝ t) : E ≃ E where
toFun := gaugeRescale s t
invFun := gaugeRescale t s
left_inv x := by rw [gaugeRescale_gaugeRescale, gaugeRescale_self_apply] <;> assumption
right_inv x := by rw [gaugeRescale_gaugeRescale, gaugeRescale_self_apply] <;> assumption
