Theorems · Definition · general topology

AddCircle.equivIccQuot

{𝕜 : Type u_1} →
  [inst : AddCommGroup 𝕜] →
    [inst_1 : LinearOrder 𝕜] →
      [inst_2 : IsOrderedAddMonoid 𝕜] →
        (p a : 𝕜) → [hp : Fact (0 < p)] → [Archimedean 𝕜] → AddCircle p ≃ Quot (AddCircle.EndpointIdent p a)

The equivalence between AddCircle p and the quotient of [a, a + p] by the relation identifying the endpoints.

Defined in

Mathlib.Topology.Instances.AddCircle.Defs

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidFactArchimedean