Theorems · Definition · convex and discrete geometry

gaugeRescaleHomeomorph

{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 →
                  s ∈ nhds 0 →
                    Bornology.IsVonNBounded ℝ s → Convex ℝ t → t ∈ nhds 0 → Bornology.IsVonNBounded ℝ t → E ≃ₜ E

gaugeRescale bundled as a Homeomorph.

Defined in

Mathlib.Analysis.Convex.GaugeRescale

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulT1Space