Theorems · Definition · general topology

iccHomeoI

{𝕜 : Type u_1} →
  [inst : Field 𝕜] →
    [inst_1 : LinearOrder 𝕜] →
      [IsStrictOrderedRing 𝕜] →
        [inst_3 : TopologicalSpace 𝕜] → [IsTopologicalRing 𝕜] → (a b : 𝕜) → a < b → ↑(Set.Icc a b) ≃ₜ ↑(Set.Icc 0 1)

The affine homeomorphism from a nontrivial interval [a,b] to [0,1].

Defined in

Mathlib.Topology.UnitInterval

Cited by

5 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingTopologicalSpaceIsTopologicalRing