English
The image of interior s under gaugeRescaleHomeomorph s t equals interior t.
Русский
Образ interior s под gaugeRescaleHomeomorph равен interior t.
LaTeX
$$$\\operatorname{image}(\\operatorname{gaugeRescaleHomeomorph}(s,t,\\dots))(\\operatorname{interior} s) = \\operatorname{interior} t$$$
Lean4
theorem image_gaugeRescaleHomeomorph_interior {s t : Set E} (hsc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) (hsb : IsVonNBounded ℝ s)
(htc : Convex ℝ t) (ht₀ : t ∈ 𝓝 0) (htb : IsVonNBounded ℝ t) :
gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb '' interior s = interior t :=
Subset.antisymm (mapsTo_gaugeRescale_interior ht₀ htc).image_subset <|
by
rw [← Homeomorph.preimage_symm, ← image_subset_iff]
exact (mapsTo_gaugeRescale_interior hs₀ hsc).image_subset