Theorems · Theorem · convex and discrete geometry

exists_homeomorph_image_interior_closure_frontier_eq_unitBall

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E},
  Convex ℝ s →
    (interior s).Nonempty →
      Bornology.IsBounded s →
        ∃ h,
          ⇑h '' interior s = Metric.ball 0 1 ∧
            ⇑h '' closure s = Metric.closedBall 0 1 ∧ ⇑h '' frontier s = Metric.sphere 0 1

If s is a convex bounded set with a nonempty interior in a real normed space, then there is a homeomorphism of the ambient space to itself that sends the interior of s to the unit open ball and the closure of s to the unit closed ball.

Defined in

Mathlib.Analysis.Convex.GaugeRescale

Cited by

0 results in Mathlib

Foundations

Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace