theorem AddCircle.liftIoc_eq_liftIco_of_ne {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] {p : 𝕜} [hp : Fact (0 < p)] {a : 𝕜} (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} [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.

theorem AddCircle.coe_eq_coe_iff_of_mem_Ioc {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {x y : 𝕜} (hx : x ∈ Set.Ioc a (a + p)) (hy : y ∈ Set.Ioc a (a + p)) : ↑x = ↑y ↔ x = y

Ioc version of mathlib coe_eq_coe_iff_of_mem_Ico

theorem AddCircle.eq_coe_Ioc {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] (a : AddCircle p) : ∃ b ∈ Set.Ioc 0 p, ↑b = a

Ioc version of mathlib eq_coe_Ico