English
Under appropriate convexity and boundedness assumptions, gaugeRescaleHomeomorph s t is a homeomorphism of E onto E.
Русский
При надлежащей выпуклости и ограниченности gaugeRescaleHomeomorph является гомеоморфизмом E на E.
LaTeX
$$$\\operatorname{gaugeRescaleHomeomorph}(s,t,\\dots) : E \\to E \\text{ is a homeomorphism}$$$
Lean4
/-- `gaugeRescale` bundled as a `Homeomorph`. -/
def gaugeRescaleHomeomorph (s t : Set E) (hsc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) (hsb : IsVonNBounded ℝ s) (htc : Convex ℝ t)
(ht₀ : t ∈ 𝓝 0) (htb : IsVonNBounded ℝ t) : E ≃ₜ E
where
toEquiv := gaugeRescaleEquiv s t (absorbent_nhds_zero hs₀) hsb (absorbent_nhds_zero ht₀) htb
continuous_toFun := by apply continuous_gaugeRescale <;> assumption
continuous_invFun := by apply continuous_gaugeRescale <;> assumption
