theorem AddCircle.liftIoc_eq_liftIco_of_ne {𝕜 : Type u_1} {B : Type u_2} [LinearOrderedAddCommGroup 𝕜] {p : 𝕜} [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] (f : 𝕜 → B) {x : AddCircle p} (x_ne_a : x ≠ ↑a) : liftIoc p a f x = liftIco p a f x

theorem AddCircle.liftIco_coe_apply_of_periodic {𝕜 : Type u_1} {B : Type u_2} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [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} [LinearOrderedAddCommGroup 𝕜] [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.