mathlib3 documentation

algebra.order.to_interval_mod

Reducing to an interval modulo its length #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines operations that reduce a number (in an archimedean linear_ordered_add_comm_group) to a number in a given interval, modulo the length of that interval.

Main definitions #

noncomputable def to_Ico_div {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :

The unique integer such that this multiple of p, subtracted from b, is in Ico a (a + p).

Equations
theorem sub_to_Ico_div_zsmul_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - to_Ico_div hp a b p set.Ico a (a + p)
theorem to_Ico_div_eq_of_sub_zsmul_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} {n : } (h : b - n p set.Ico a (a + p)) :
to_Ico_div hp a b = n
noncomputable def to_Ioc_div {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :

The unique integer such that this multiple of p, subtracted from b, is in Ioc a (a + p).

Equations
theorem sub_to_Ioc_div_zsmul_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - to_Ioc_div hp a b p set.Ioc a (a + p)
theorem to_Ioc_div_eq_of_sub_zsmul_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} {n : } (h : b - n p set.Ioc a (a + p)) :
to_Ioc_div hp a b = n
noncomputable def to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
α

Reduce b to the interval Ico a (a + p).

Equations
noncomputable def to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
α

Reduce b to the interval Ioc a (a + p).

Equations
theorem to_Ico_mod_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp a b set.Ico a (a + p)
theorem to_Ico_mod_mem_Ico' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (b : α) :
theorem to_Ioc_mod_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp a b set.Ioc a (a + p)
theorem left_le_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a to_Ico_mod hp a b
theorem left_lt_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
a < to_Ioc_mod hp a b
theorem to_Ico_mod_lt_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp a b < a + p
theorem to_Ioc_mod_le_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp a b a + p
@[simp]
theorem self_sub_to_Ico_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - to_Ico_div hp a b p = to_Ico_mod hp a b
@[simp]
theorem self_sub_to_Ioc_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - to_Ioc_div hp a b p = to_Ioc_mod hp a b
@[simp]
theorem to_Ico_div_zsmul_sub_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp a b p - b = -to_Ico_mod hp a b
@[simp]
theorem to_Ioc_div_zsmul_sub_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp a b p - b = -to_Ioc_mod hp a b
@[simp]
theorem to_Ico_mod_sub_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp a b - b = -to_Ico_div hp a b p
@[simp]
theorem to_Ioc_mod_sub_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp a b - b = -to_Ioc_div hp a b p
@[simp]
theorem self_sub_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - to_Ico_mod hp a b = to_Ico_div hp a b p
@[simp]
theorem self_sub_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
b - to_Ioc_mod hp a b = to_Ioc_div hp a b p
@[simp]
theorem to_Ico_mod_add_to_Ico_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp a b + to_Ico_div hp a b p = b
@[simp]
theorem to_Ioc_mod_add_to_Ioc_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp a b + to_Ioc_div hp a b p = b
@[simp]
theorem to_Ico_div_zsmul_sub_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp a b p + to_Ico_mod hp a b = b
@[simp]
theorem to_Ioc_div_zsmul_sub_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp a b p + to_Ioc_mod hp a b = b
theorem to_Ico_mod_eq_iff {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
to_Ico_mod hp a b = c c set.Ico a (a + p) (z : ), b = c + z p
theorem to_Ioc_mod_eq_iff {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
to_Ioc_mod hp a b = c c set.Ioc a (a + p) (z : ), b = c + z p
@[simp]
theorem to_Ico_div_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
to_Ico_div hp a a = 0
@[simp]
theorem to_Ioc_div_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
to_Ioc_div hp a a = -1
@[simp]
theorem to_Ico_mod_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
to_Ico_mod hp a a = a
@[simp]
theorem to_Ioc_mod_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
to_Ioc_mod hp a a = a + p
theorem to_Ico_div_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
to_Ico_div hp a (a + p) = 1
theorem to_Ioc_div_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
to_Ioc_div hp a (a + p) = 0
theorem to_Ico_mod_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
to_Ico_mod hp a (a + p) = a
theorem to_Ioc_mod_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
to_Ioc_mod hp a (a + p) = a + p
@[simp]
theorem to_Ico_div_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ico_div hp a (b + m p) = to_Ico_div hp a b + m
@[simp]
theorem to_Ico_div_add_zsmul' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ico_div hp (a + m p) b = to_Ico_div hp a b - m
@[simp]
theorem to_Ioc_div_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ioc_div hp a (b + m p) = to_Ioc_div hp a b + m
@[simp]
theorem to_Ioc_div_add_zsmul' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ioc_div hp (a + m p) b = to_Ioc_div hp a b - m
@[simp]
theorem to_Ico_div_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ico_div hp a (m p + b) = m + to_Ico_div hp a b

Note we omit to_Ico_div_zsmul_add' as -m + to_Ico_div hp a b is not very convenient.

@[simp]
theorem to_Ioc_div_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ioc_div hp a (m p + b) = m + to_Ioc_div hp a b

Note we omit to_Ioc_div_zsmul_add' as -m + to_Ioc_div hp a b is not very convenient.

@[simp]
theorem to_Ico_div_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ico_div hp a (b - m p) = to_Ico_div hp a b - m
@[simp]
theorem to_Ico_div_sub_zsmul' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ico_div hp (a - m p) b = to_Ico_div hp a b + m
@[simp]
theorem to_Ioc_div_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ioc_div hp a (b - m p) = to_Ioc_div hp a b - m
@[simp]
theorem to_Ioc_div_sub_zsmul' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ioc_div hp (a - m p) b = to_Ioc_div hp a b + m
@[simp]
theorem to_Ico_div_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp a (b + p) = to_Ico_div hp a b + 1
@[simp]
theorem to_Ico_div_add_right' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp (a + p) b = to_Ico_div hp a b - 1
@[simp]
theorem to_Ioc_div_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp a (b + p) = to_Ioc_div hp a b + 1
@[simp]
theorem to_Ioc_div_add_right' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp (a + p) b = to_Ioc_div hp a b - 1
@[simp]
theorem to_Ico_div_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp a (p + b) = to_Ico_div hp a b + 1
@[simp]
theorem to_Ico_div_add_left' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp (p + a) b = to_Ico_div hp a b - 1
@[simp]
theorem to_Ioc_div_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp a (p + b) = to_Ioc_div hp a b + 1
@[simp]
theorem to_Ioc_div_add_left' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp (p + a) b = to_Ioc_div hp a b - 1
@[simp]
theorem to_Ico_div_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp a (b - p) = to_Ico_div hp a b - 1
@[simp]
theorem to_Ico_div_sub' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp (a - p) b = to_Ico_div hp a b + 1
@[simp]
theorem to_Ioc_div_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp a (b - p) = to_Ioc_div hp a b - 1
@[simp]
theorem to_Ioc_div_sub' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp (a - p) b = to_Ioc_div hp a b + 1
theorem to_Ico_div_sub_eq_to_Ico_div_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
to_Ico_div hp a (b - c) = to_Ico_div hp (a + c) b
theorem to_Ioc_div_sub_eq_to_Ioc_div_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
to_Ioc_div hp a (b - c) = to_Ioc_div hp (a + c) b
theorem to_Ico_div_sub_eq_to_Ico_div_add' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
to_Ico_div hp (a - c) b = to_Ico_div hp a (b + c)
theorem to_Ioc_div_sub_eq_to_Ioc_div_add' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
to_Ioc_div hp (a - c) b = to_Ioc_div hp a (b + c)
theorem to_Ico_div_neg {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp a (-b) = -(to_Ioc_div hp (-a) b + 1)
theorem to_Ico_div_neg' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp (-a) b = -(to_Ioc_div hp a (-b) + 1)
theorem to_Ioc_div_neg {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp a (-b) = -(to_Ico_div hp (-a) b + 1)
theorem to_Ioc_div_neg' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp (-a) b = -(to_Ico_div hp a (-b) + 1)
@[simp]
theorem to_Ico_mod_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ico_mod hp a (b + m p) = to_Ico_mod hp a b
@[simp]
theorem to_Ico_mod_add_zsmul' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ico_mod hp (a + m p) b = to_Ico_mod hp a b + m p
@[simp]
theorem to_Ioc_mod_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ioc_mod hp a (b + m p) = to_Ioc_mod hp a b
@[simp]
theorem to_Ioc_mod_add_zsmul' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ioc_mod hp (a + m p) b = to_Ioc_mod hp a b + m p
@[simp]
theorem to_Ico_mod_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ico_mod hp a (m p + b) = to_Ico_mod hp a b
@[simp]
theorem to_Ico_mod_zsmul_add' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ico_mod hp (m p + a) b = m p + to_Ico_mod hp a b
@[simp]
theorem to_Ioc_mod_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ioc_mod hp a (m p + b) = to_Ioc_mod hp a b
@[simp]
theorem to_Ioc_mod_zsmul_add' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ioc_mod hp (m p + a) b = m p + to_Ioc_mod hp a b
@[simp]
theorem to_Ico_mod_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ico_mod hp a (b - m p) = to_Ico_mod hp a b
@[simp]
theorem to_Ico_mod_sub_zsmul' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ico_mod hp (a - m p) b = to_Ico_mod hp a b - m p
@[simp]
theorem to_Ioc_mod_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ioc_mod hp a (b - m p) = to_Ioc_mod hp a b
@[simp]
theorem to_Ioc_mod_sub_zsmul' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ) :
to_Ioc_mod hp (a - m p) b = to_Ioc_mod hp a b - m p
@[simp]
theorem to_Ico_mod_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp a (b + p) = to_Ico_mod hp a b
@[simp]
theorem to_Ico_mod_add_right' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp (a + p) b = to_Ico_mod hp a b + p
@[simp]
theorem to_Ioc_mod_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp a (b + p) = to_Ioc_mod hp a b
@[simp]
theorem to_Ioc_mod_add_right' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp (a + p) b = to_Ioc_mod hp a b + p
@[simp]
theorem to_Ico_mod_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp a (p + b) = to_Ico_mod hp a b
@[simp]
theorem to_Ico_mod_add_left' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp (p + a) b = p + to_Ico_mod hp a b
@[simp]
theorem to_Ioc_mod_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp a (p + b) = to_Ioc_mod hp a b
@[simp]
theorem to_Ioc_mod_add_left' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp (p + a) b = p + to_Ioc_mod hp a b
@[simp]
theorem to_Ico_mod_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp a (b - p) = to_Ico_mod hp a b
@[simp]
theorem to_Ico_mod_sub' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp (a - p) b = to_Ico_mod hp a b - p
@[simp]
theorem to_Ioc_mod_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp a (b - p) = to_Ioc_mod hp a b
@[simp]
theorem to_Ioc_mod_sub' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp (a - p) b = to_Ioc_mod hp a b - p
theorem to_Ico_mod_sub_eq_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
to_Ico_mod hp a (b - c) = to_Ico_mod hp (a + c) b - c
theorem to_Ioc_mod_sub_eq_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
to_Ioc_mod hp a (b - c) = to_Ioc_mod hp (a + c) b - c
theorem to_Ico_mod_add_right_eq_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
to_Ico_mod hp a (b + c) = to_Ico_mod hp (a - c) b + c
theorem to_Ioc_mod_add_right_eq_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b c : α) :
to_Ioc_mod hp a (b + c) = to_Ioc_mod hp (a - c) b + c
theorem to_Ico_mod_neg {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp a (-b) = p - to_Ioc_mod hp (-a) b
theorem to_Ico_mod_neg' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp (-a) b = p - to_Ioc_mod hp a (-b)
theorem to_Ioc_mod_neg {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp a (-b) = p - to_Ico_mod hp (-a) b
theorem to_Ioc_mod_neg' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp (-a) b = p - to_Ico_mod hp a (-b)
theorem to_Ico_mod_eq_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
to_Ico_mod hp a b = to_Ico_mod hp a c (n : ), c - b = n p
theorem to_Ioc_mod_eq_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
to_Ioc_mod hp a b = to_Ioc_mod hp a c (n : ), c - b = n p
theorem add_comm_group.modeq_iff_to_Ico_mod_eq_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] to_Ico_mod hp a b = a
theorem add_comm_group.modeq_iff_to_Ioc_mod_eq_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] to_Ioc_mod hp a b = a + p
theorem add_comm_group.modeq.to_Ico_mod_eq_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] to_Ico_mod hp a b = a

Alias of the forward direction of add_comm_group.modeq_iff_to_Ico_mod_eq_left.

theorem add_comm_group.modeq.to_Ico_mod_eq_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] to_Ioc_mod hp a b = a + p

Alias of the forward direction of add_comm_group.modeq_iff_to_Ioc_mod_eq_right.

theorem add_comm_group.tfae_modeq {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
[a b [PMOD p], (z : ), b - z p set.Ioo a (a + p), to_Ico_mod hp a b to_Ioc_mod hp a b, to_Ico_mod hp a b + p = to_Ioc_mod hp a b].tfae
theorem add_comm_group.modeq_iff_not_forall_mem_Ioo_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] (z : ), b - z p set.Ioo a (a + p)
theorem add_comm_group.modeq_iff_to_Ico_mod_ne_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] to_Ico_mod hp a b to_Ioc_mod hp a b
theorem add_comm_group.modeq_iff_to_Ico_mod_add_period_eq_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] to_Ico_mod hp a b + p = to_Ioc_mod hp a b
theorem add_comm_group.not_modeq_iff_to_Ico_mod_eq_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
¬a b [PMOD p] to_Ico_mod hp a b = to_Ioc_mod hp a b
theorem add_comm_group.not_modeq_iff_to_Ico_div_eq_to_Ioc_div {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
¬a b [PMOD p] to_Ico_div hp a b = to_Ioc_div hp a b
theorem add_comm_group.modeq_iff_to_Ico_div_eq_to_Ioc_div_add_one {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
a b [PMOD p] to_Ico_div hp a b = to_Ioc_div hp a b + 1
@[simp]
theorem to_Ico_mod_inj {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
to_Ico_mod hp c a = to_Ico_mod hp c b a b [PMOD p]

If a and b fall within the same cycle WRT c, then they are congruent modulo p.

theorem add_comm_group.modeq.to_Ico_mod_eq_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b c : α} :
a b [PMOD p] to_Ico_mod hp c a = to_Ico_mod hp c b

Alias of the reverse direction of to_Ico_mod_inj.

theorem Ico_eq_locus_Ioc_eq_Union_Ioo {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a : α} :
{b : α | to_Ico_mod hp a b = to_Ioc_mod hp a b} = (z : ), set.Ioo (a + z p) (a + p + z p)
theorem to_Ioc_div_wcovby_to_Ico_div {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp a b ⩿ to_Ico_div hp a b
theorem to_Ico_mod_le_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp a b to_Ioc_mod hp a b
theorem to_Ioc_mod_le_to_Ico_mod_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp a b to_Ico_mod hp a b + p
theorem to_Ico_mod_eq_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
to_Ico_mod hp a b = b b set.Ico a (a + p)
theorem to_Ioc_mod_eq_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) {a b : α} :
to_Ioc_mod hp a b = b b set.Ioc a (a + p)
@[simp]
theorem to_Ico_mod_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a₁ a₂ b : α) :
to_Ico_mod hp a₁ (to_Ico_mod hp a₂ b) = to_Ico_mod hp a₁ b
@[simp]
theorem to_Ico_mod_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a₁ a₂ b : α) :
to_Ico_mod hp a₁ (to_Ioc_mod hp a₂ b) = to_Ico_mod hp a₁ b
@[simp]
theorem to_Ioc_mod_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a₁ a₂ b : α) :
to_Ioc_mod hp a₁ (to_Ioc_mod hp a₂ b) = to_Ioc_mod hp a₁ b
@[simp]
theorem to_Ioc_mod_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a₁ a₂ b : α) :
to_Ioc_mod hp a₁ (to_Ico_mod hp a₂ b) = to_Ioc_mod hp a₁ b
theorem to_Ico_mod_periodic {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
theorem to_Ioc_mod_periodic {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
theorem to_Ico_mod_zero_sub_comm {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp 0 (a - b) = p - to_Ioc_mod hp 0 (b - a)
theorem to_Ioc_mod_zero_sub_comm {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp 0 (a - b) = p - to_Ico_mod hp 0 (b - a)
theorem to_Ico_div_eq_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp a b = to_Ico_div hp 0 (b - a)
theorem to_Ioc_div_eq_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp a b = to_Ioc_div hp 0 (b - a)
theorem to_Ico_mod_eq_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp a b = to_Ico_mod hp 0 (b - a) + a
theorem to_Ioc_mod_eq_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp a b = to_Ioc_mod hp 0 (b - a) + a
theorem to_Ico_mod_add_to_Ioc_mod_zero {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp 0 (a - b) + to_Ioc_mod hp 0 (b - a) = p
theorem to_Ioc_mod_add_to_Ico_mod_zero {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp 0 (a - b) + to_Ico_mod hp 0 (b - a) = p
@[simp]
theorem quotient_add_group.equiv_Ico_mod_symm_apply {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) (ᾰ : (set.Ico a (a + p))) :
noncomputable def quotient_add_group.equiv_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :

to_Ico_mod as an equiv from the quotient.

Equations
@[simp]
theorem quotient_add_group.equiv_Ico_mod_coe {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
@[simp]
theorem quotient_add_group.equiv_Ico_mod_zero {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :
noncomputable def quotient_add_group.equiv_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :

to_Ioc_mod as an equiv from the quotient.

Equations
@[simp]
theorem quotient_add_group.equiv_Ioc_mod_symm_apply {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) (ᾰ : (set.Ioc a (a + p))) :
@[simp]
theorem quotient_add_group.equiv_Ioc_mod_coe {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a b : α) :
@[simp]
theorem quotient_add_group.equiv_Ioc_mod_zero {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} (hp : 0 < p) (a : α) :

The circular order structure on α ⧸ add_subgroup.zmultiples p #

@[protected, instance]
Equations
theorem quotient_add_group.btw_coe_iff' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} [hp' : fact (0 < p)] {x₁ x₂ x₃ : α} :
has_btw.btw x₁ x₂ x₃ to_Ico_mod _ 0 (x₂ - x₁) to_Ioc_mod _ 0 (x₃ - x₁)
theorem quotient_add_group.btw_coe_iff {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {p : α} [hp' : fact (0 < p)] {x₁ x₂ x₃ : α} :
has_btw.btw x₁ x₂ x₃ to_Ico_mod _ x₁ x₂ to_Ioc_mod _ x₁ x₃

Connections to int.floor and int.fract #

theorem to_Ico_div_eq_floor {α : Type u_1} [linear_ordered_field α] [floor_ring α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_div hp a b = (b - a) / p
theorem to_Ioc_div_eq_neg_floor {α : Type u_1} [linear_ordered_field α] [floor_ring α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_div hp a b = -(a + p - b) / p
theorem to_Ico_div_zero_one {α : Type u_1} [linear_ordered_field α] [floor_ring α] (b : α) :
theorem to_Ico_mod_eq_add_fract_mul {α : Type u_1} [linear_ordered_field α] [floor_ring α] {p : α} (hp : 0 < p) (a b : α) :
to_Ico_mod hp a b = a + int.fract ((b - a) / p) * p
theorem to_Ico_mod_eq_fract_mul {α : Type u_1} [linear_ordered_field α] [floor_ring α] {p : α} (hp : 0 < p) (b : α) :
to_Ico_mod hp 0 b = int.fract (b / p) * p
theorem to_Ioc_mod_eq_sub_fract_mul {α : Type u_1} [linear_ordered_field α] [floor_ring α] {p : α} (hp : 0 < p) (a b : α) :
to_Ioc_mod hp a b = a + p - int.fract ((a + p - b) / p) * p
theorem to_Ico_mod_zero_one {α : Type u_1} [linear_ordered_field α] [floor_ring α] (b : α) :

Lemmas about unions of translates of intervals #

theorem Union_Ioc_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {p : α} (hp : 0 < p) (a : α) :
( (n : ), set.Ioc (a + n p) (a + (n + 1) p)) = set.univ
theorem Union_Ico_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {p : α} (hp : 0 < p) (a : α) :
( (n : ), set.Ico (a + n p) (a + (n + 1) p)) = set.univ
theorem Union_Icc_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {p : α} (hp : 0 < p) (a : α) :
( (n : ), set.Icc (a + n p) (a + (n + 1) p)) = set.univ
theorem Union_Ioc_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {p : α} (hp : 0 < p) :
( (n : ), set.Ioc (n p) ((n + 1) p)) = set.univ
theorem Union_Ico_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {p : α} (hp : 0 < p) :
( (n : ), set.Ico (n p) ((n + 1) p)) = set.univ
theorem Union_Icc_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {p : α} (hp : 0 < p) :
( (n : ), set.Icc (n p) ((n + 1) p)) = set.univ
theorem Union_Ioc_add_int_cast {α : Type u_1} [linear_ordered_ring α] [archimedean α] (a : α) :
( (n : ), set.Ioc (a + n) (a + n + 1)) = set.univ
theorem Union_Ico_add_int_cast {α : Type u_1} [linear_ordered_ring α] [archimedean α] (a : α) :
( (n : ), set.Ico (a + n) (a + n + 1)) = set.univ
theorem Union_Icc_add_int_cast {α : Type u_1} [linear_ordered_ring α] [archimedean α] (a : α) :
( (n : ), set.Icc (a + n) (a + n + 1)) = set.univ
theorem Union_Ioc_int_cast (α : Type u_1) [linear_ordered_ring α] [archimedean α] :
( (n : ), set.Ioc n (n + 1)) = set.univ
theorem Union_Ico_int_cast (α : Type u_1) [linear_ordered_ring α] [archimedean α] :
( (n : ), set.Ico n (n + 1)) = set.univ
theorem Union_Icc_int_cast (α : Type u_1) [linear_ordered_ring α] [archimedean α] :
( (n : ), set.Icc n (n + 1)) = set.univ