Theorems · Definition · general topology

AddCircle.equivIco

{𝕜 : Type u_1} →
  [inst : AddCommGroup 𝕜] →
    (p : 𝕜) →
      [inst_1 : LinearOrder 𝕜] →
        [IsOrderedAddMonoid 𝕜] → [hp : Fact (0 < p)] → (a : 𝕜) → [Archimedean 𝕜] → AddCircle p ≃ ↑(Set.Ico a (a + p))

The equivalence between AddCircle p and the half-open interval [a, a + p), whose inverse is the natural quotient map.

Defined in

Mathlib.Topology.Instances.AddCircle.Defs

Cited by

11 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidFactArchimedean