English
The image of closure s under gaugeRescaleHomeomorph s t equals closure t.
Русский
Образ closure s под gaugeRescaleHomeomorph равен closure t.
LaTeX
$$$\\operatorname{image}(\\operatorname{gaugeRescaleHomeomorph}(s,t,\\dots))(\\operatorname{closure} s) = \\operatorname{closure} t$$$
Lean4
theorem image_gaugeRescaleHomeomorph_closure {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 '' closure s = closure t :=
by
refine
Subset.antisymm
(mapsTo_gaugeRescale_closure hsc hs₀ htc (mem_of_mem_nhds ht₀) (absorbent_nhds_zero ht₀)).image_subset ?_
rw [← Homeomorph.preimage_symm, ← image_subset_iff]
exact (mapsTo_gaugeRescale_closure htc ht₀ hsc (mem_of_mem_nhds hs₀) (absorbent_nhds_zero hs₀)).image_subset
