Theorems · Definition · general topology

AddCircle.equivIoc

{𝕜 : Type u_1} →
  [inst : AddCommGroup 𝕜] →
    (p : 𝕜) →
      [inst_1 : LinearOrder 𝕜] →
        [IsOrderedAddMonoid 𝕜] → [hp : Fact (0 < p)] → (a : 𝕜) → [Archimedean 𝕜] → AddCircle p ≃ ↑(Set.Ioc 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

12 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidFactArchimedean