English
Under convexity and absorbent conditions, gaugeRescale maps closure s into closure t.
Русский
При выпуклости и абсорбентности gaugeRescale отображает closure s в closure t.
LaTeX
$$MapsTo (gaugeRescale s t) (closure s) (closure t)$$
Lean4
theorem mapsTo_gaugeRescale_closure {s t : Set E} (hsc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) (htc : Convex ℝ t) (ht₀ : 0 ∈ t)
(hta : Absorbent ℝ t) : MapsTo (gaugeRescale s t) (closure s) (closure t) := fun _x hx ↦
mem_closure_of_gauge_le_one htc ht₀ hta <|
(gauge_gaugeRescale_le _ _ _).trans <| (gauge_le_one_iff_mem_closure hsc hs₀).2 hx