Theorems · Definition · general topology

AddCircle.liftIco

{𝕜 : Type u_1} →
  {B : Type u_2} →
    [inst : AddCommGroup 𝕜] →
      (p : 𝕜) →
        [inst_1 : LinearOrder 𝕜] →
          [IsOrderedAddMonoid 𝕜] → [hp : Fact (0 < p)] → 𝕜 → [Archimedean 𝕜] → (𝕜 → B) → AddCircle p → B

Given a function on 𝕜, return the unique function on AddCircle p agreeing with f on [a, a + p).

Defined in

Mathlib.Topology.Instances.AddCircle.Defs

Cited by

10 results in Mathlib

Foundations

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

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidFactArchimedean