image_gaugeRescaleHomeomorph_interior

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

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