mapsTo_gaugeRescale_interior — Mathlib

English

Under convexity and absorbent/nature conditions, gaugeRescale maps interior s into interior t.

Русский

При выпуклости и условиях абсорбентности и VonNeumann-ограниченности gaugeRescale переводит interior s в interior t.

LaTeX

$$MapsTo (gaugeRescale s t) (interior s) (interior t)$$

Lean4

theorem mapsTo_gaugeRescale_interior (h₀ : t ∈ 𝓝 0) (hc : Convex ℝ t) :
    MapsTo (gaugeRescale s t) (interior s) (interior t) := fun x hx ↦
  by
  rw [← gauge_lt_one_iff_mem_interior] <;> try assumption
  exact (gauge_gaugeRescale_le _ _ _).trans_lt (interior_subset_gauge_lt_one _ hx)

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