Theorems · Theorem · convex and discrete geometry

exists_homeomorph_image_eq

∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E] [T1Space E] {s t : Set E},
  Convex ℝ s →
    (interior s).Nonempty →
      Bornology.IsVonNBounded ℝ s →
        Convex ℝ t →
          (interior t).Nonempty →
            Bornology.IsVonNBounded ℝ t →
              ∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure s = closure t ∧ ⇑e '' frontier s = frontier t

Given two convex bounded sets in a topological vector space with nonempty interiors, there exists a homeomorphism of the ambient space that sends the interior, the closure, and the frontier of one set to the interior, the closure, and the frontier of the other set. In particular, if both s and t are open set or both s and t are closed sets, then e maps s to t.

Defined in

Mathlib.Analysis.Convex.GaugeRescale

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulT1Space