theorem AddCircle.liftIco_coe_apply_of_periodic {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) (x : 𝕜) : liftIco p a f ↑x = f x

theorem AddCircle.liftIoc_coe_apply_of_periodic {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) (x : 𝕜) : liftIoc p a f ↑x = f x

theorem AddCircle.liftIco_comp_mk_eq_of_periodic {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) : liftIco p a f ∘ QuotientAddGroup.mk = f

theorem AddCircle.liftIoc_comp_mk_eq_of_periodic {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) : liftIoc p a f ∘ QuotientAddGroup.mk = f

theorem AddCircle.liftIco_eq_liftIco {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a a' : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) : liftIco p a f = liftIco p a' f

If f has period p, then every lift of f to AddCircle p is the same.

theorem AddCircle.liftIoc_eq_liftIoc {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a a' : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) : liftIoc p a f = liftIoc p a' f

If f has period p, then every lift of f to AddCircle p is the same.

theorem AddCircle.liftIco_eq_liftIoc {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] (a a' : 𝕜) {f : 𝕜 → B} (hf : Function.Periodic f p) : liftIco p a f = liftIoc p a' f

If f has period p, then every lift of f to AddCircle p is the same.