mathlib documentation

algebra.order.to_interval_mod

Reducing to an interval modulo its length #

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 α] (a : α) {b : α} (hb : 0 < b) (x : α) :

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

Equations
theorem sub_to_Ico_div_zsmul_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x - to_Ico_div a hb x b set.Ico a (a + b)
theorem eq_to_Ico_div_of_sub_zsmul_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b x : α} (hb : 0 < b) {y : } (hy : x - y b set.Ico a (a + b)) :
y = to_Ico_div a hb x
noncomputable def to_Ioc_div {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :

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

Equations
theorem sub_to_Ioc_div_zsmul_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x - to_Ioc_div a hb x b set.Ioc a (a + b)
theorem eq_to_Ioc_div_of_sub_zsmul_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b x : α} (hb : 0 < b) {y : } (hy : x - y b set.Ioc a (a + b)) :
y = to_Ioc_div a hb x
noncomputable def to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
α

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

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

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

Equations
theorem to_Ico_mod_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb x set.Ico a (a + b)
theorem to_Ico_mod_mem_Ico' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {b : α} (hb : 0 < b) (x : α) :
theorem to_Ioc_mod_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb x set.Ioc a (a + b)
theorem left_le_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
a to_Ico_mod a hb x
theorem left_lt_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
a < to_Ioc_mod a hb x
theorem to_Ico_mod_lt_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb x < a + b
theorem to_Ioc_mod_le_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb x a + b
@[simp]
theorem self_sub_to_Ico_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x - to_Ico_div a hb x b = to_Ico_mod a hb x
@[simp]
theorem self_sub_to_Ioc_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x - to_Ioc_div a hb x b = to_Ioc_mod a hb x
@[simp]
theorem to_Ico_div_zsmul_sub_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb x b - x = -to_Ico_mod a hb x
@[simp]
theorem to_Ioc_div_zsmul_sub_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb x b - x = -to_Ioc_mod a hb x
@[simp]
theorem to_Ico_mod_sub_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb x - x = -to_Ico_div a hb x b
@[simp]
theorem to_Ioc_mod_sub_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb x - x = -to_Ioc_div a hb x b
@[simp]
theorem self_sub_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x - to_Ico_mod a hb x = to_Ico_div a hb x b
@[simp]
theorem self_sub_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x - to_Ioc_mod a hb x = to_Ioc_div a hb x b
@[simp]
theorem to_Ico_mod_add_to_Ico_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb x + to_Ico_div a hb x b = x
@[simp]
theorem to_Ioc_mod_add_to_Ioc_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb x + to_Ioc_div a hb x b = x
@[simp]
theorem to_Ico_div_zsmul_sub_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb x b + to_Ico_mod a hb x = x
@[simp]
theorem to_Ioc_div_zsmul_sub_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb x b + to_Ioc_mod a hb x = x
theorem to_Ico_mod_eq_iff {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b x y : α} (hb : 0 < b) :
to_Ico_mod a hb x = y y set.Ico a (a + b) (z : ), x = y + z b
theorem to_Ioc_mod_eq_iff {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b x y : α} (hb : 0 < b) :
to_Ioc_mod a hb x = y y set.Ioc a (a + b) (z : ), x = y + z b
@[simp]
theorem to_Ico_div_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ico_div a hb a = 0
@[simp]
theorem to_Ioc_div_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ioc_div a hb a = -1
@[simp]
theorem to_Ico_mod_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ico_mod a hb a = a
@[simp]
theorem to_Ioc_mod_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ioc_mod a hb a = a + b
theorem to_Ico_div_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ico_div a hb (a + b) = 1
theorem to_Ioc_div_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ioc_div a hb (a + b) = 0
theorem to_Ico_mod_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ico_mod a hb (a + b) = a
theorem to_Ioc_mod_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ioc_mod a hb (a + b) = a + b
@[simp]
theorem to_Ico_div_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ico_div a hb (x + m b) = to_Ico_div a hb x + m
@[simp]
theorem to_Ioc_div_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ioc_div a hb (x + m b) = to_Ioc_div a hb x + m
@[simp]
theorem to_Ico_div_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ico_div a hb (m b + x) = m + to_Ico_div a hb x
@[simp]
theorem to_Ioc_div_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ioc_div a hb (m b + x) = to_Ioc_div a hb x + m
@[simp]
theorem to_Ico_div_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ico_div a hb (x - m b) = to_Ico_div a hb x - m
@[simp]
theorem to_Ioc_div_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ioc_div a hb (x - m b) = to_Ioc_div a hb x - m
@[simp]
theorem to_Ico_div_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb (x + b) = to_Ico_div a hb x + 1
@[simp]
theorem to_Ioc_div_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb (x + b) = to_Ioc_div a hb x + 1
@[simp]
theorem to_Ico_div_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb (b + x) = to_Ico_div a hb x + 1
@[simp]
theorem to_Ioc_div_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb (b + x) = to_Ioc_div a hb x + 1
@[simp]
theorem to_Ico_div_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb (x - b) = to_Ico_div a hb x - 1
@[simp]
theorem to_Ioc_div_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb (x - b) = to_Ioc_div a hb x - 1
theorem to_Ico_div_sub' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x y : α) :
to_Ico_div a hb (x - y) = to_Ico_div (a + y) hb x
theorem to_Ioc_div_sub' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x y : α) :
to_Ioc_div a hb (x - y) = to_Ioc_div (a + y) hb x
theorem to_Ico_div_add_right' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x y : α) :
to_Ico_div a hb (x + y) = to_Ico_div (a - y) hb x
theorem to_Ioc_div_add_right' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x y : α) :
to_Ioc_div a hb (x + y) = to_Ioc_div (a - y) hb x
theorem to_Ico_div_neg {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb (-x) = -(to_Ioc_div (-a) hb x + 1)
theorem to_Ioc_div_neg {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb (-x) = -(to_Ico_div (-a) hb x + 1)
@[simp]
theorem to_Ico_mod_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ico_mod a hb (x + m b) = to_Ico_mod a hb x
@[simp]
theorem to_Ioc_mod_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ioc_mod a hb (x + m b) = to_Ioc_mod a hb x
@[simp]
theorem to_Ico_mod_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ico_mod a hb (m b + x) = to_Ico_mod a hb x
@[simp]
theorem to_Ioc_mod_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ioc_mod a hb (m b + x) = to_Ioc_mod a hb x
@[simp]
theorem to_Ico_mod_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ico_mod a hb (x - m b) = to_Ico_mod a hb x
@[simp]
theorem to_Ioc_mod_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ) :
to_Ioc_mod a hb (x - m b) = to_Ioc_mod a hb x
@[simp]
theorem to_Ico_mod_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb (x + b) = to_Ico_mod a hb x
@[simp]
theorem to_Ioc_mod_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb (x + b) = to_Ioc_mod a hb x
@[simp]
theorem to_Ico_mod_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb (b + x) = to_Ico_mod a hb x
@[simp]
theorem to_Ioc_mod_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb (b + x) = to_Ioc_mod a hb x
@[simp]
theorem to_Ico_mod_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb (x - b) = to_Ico_mod a hb x
@[simp]
theorem to_Ioc_mod_sub {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb (x - b) = to_Ioc_mod a hb x
theorem to_Ico_mod_sub' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x y : α) :
to_Ico_mod a hb (x - y) = to_Ico_mod (a + y) hb x - y
theorem to_Ioc_mod_sub' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x y : α) :
to_Ioc_mod a hb (x - y) = to_Ioc_mod (a + y) hb x - y
theorem to_Ico_mod_add_right' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x y : α) :
to_Ico_mod a hb (x + y) = to_Ico_mod (a - y) hb x + y
theorem to_Ioc_mod_add_right' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x y : α) :
to_Ioc_mod a hb (x + y) = to_Ioc_mod (a - y) hb x + y
theorem to_Ico_mod_neg {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb (-x) = b - to_Ioc_mod (-a) hb x
theorem to_Ioc_mod_neg {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb (-x) = b - to_Ico_mod (-a) hb x
theorem to_Ico_mod_eq_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b x y : α} (hb : 0 < b) :
to_Ico_mod a hb x = to_Ico_mod a hb y (z : ), y - x = z b
theorem to_Ioc_mod_eq_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b x y : α} (hb : 0 < b) :
to_Ioc_mod a hb x = to_Ioc_mod a hb y (z : ), y - x = z b
def mem_Ioo_mod {α : Type u_1} [linear_ordered_add_comm_group α] (a b x : α) :
Prop

mem_Ioo_mod a b x means that x lies in the open interval (a, a + b) modulo b. Equivalently (as shown below), x is not congruent to a modulo b, or to_Ico_mod a hb agrees with to_Ioc_mod a hb at x, or to_Ico_div a hb agrees with to_Ioc_div a hb at x.

Equations
theorem tfae_mem_Ioo_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
[mem_Ioo_mod a b x, to_Ico_mod a hb x = to_Ioc_mod a hb x, to_Ico_mod a hb x + b to_Ioc_mod a hb x, to_Ico_mod a hb x a].tfae
theorem mem_Ioo_mod_iff_to_Ico_mod_eq_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
mem_Ioo_mod a b x to_Ico_mod a hb x = to_Ioc_mod a hb x
theorem mem_Ioo_mod_iff_to_Ico_mod_add_period_ne_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
mem_Ioo_mod a b x to_Ico_mod a hb x + b to_Ioc_mod a hb x
theorem mem_Ioo_mod_iff_to_Ico_mod_ne_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
mem_Ioo_mod a b x to_Ico_mod a hb x a
theorem not_mem_Ioo_mod_iff_to_Ico_mod_add_period_eq_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
¬mem_Ioo_mod a b x to_Ico_mod a hb x + b = to_Ioc_mod a hb x
theorem not_mem_Ioo_mod_iff_to_Ico_mod_eq_left {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
¬mem_Ioo_mod a b x to_Ico_mod a hb x = a
theorem mem_Ioo_mod_iff_to_Ioc_mod_ne_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
mem_Ioo_mod a b x to_Ioc_mod a hb x a + b
theorem not_mem_Ioo_mod_iff_to_Ioc_eq_right {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
¬mem_Ioo_mod a b x to_Ioc_mod a hb x = a + b
theorem mem_Ioo_mod_iff_to_Ico_div_eq_to_Ioc_div {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
mem_Ioo_mod a b x to_Ico_div a hb x = to_Ioc_div a hb x
theorem mem_Ioo_mod_iff_to_Ico_div_ne_to_Ioc_div_add_one {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
mem_Ioo_mod a b x to_Ico_div a hb x to_Ioc_div a hb x + 1
theorem not_mem_Ioo_mod_iff_to_Ico_div_eq_to_Ioc_div_add_one {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
¬mem_Ioo_mod a b x to_Ico_div a hb x = to_Ioc_div a hb x + 1
theorem mem_Ioo_mod_iff_ne_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
mem_Ioo_mod a b x (z : ), x a + z b
theorem not_mem_Ioo_mod_iff_eq_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
¬mem_Ioo_mod a b x (z : ), x = a + z b
theorem not_mem_Ioo_mod_iff_eq_mod_zmultiples {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
theorem mem_Ioo_mod_iff_ne_mod_zmultiples {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
theorem Ico_eq_locus_Ioc_eq_Union_Ioo {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) :
{x : α | to_Ico_mod a hb x = to_Ioc_mod a hb x} = (z : ), set.Ioo (a + z b) (a + b + z b)
theorem to_Ioc_div_wcovby_to_Ico_div {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb x ⩿ to_Ico_div a hb x
theorem to_Ico_mod_le_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb x to_Ioc_mod a hb x
theorem to_Ioc_mod_le_to_Ico_mod_add {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb x to_Ico_mod a hb x + b
theorem to_Ico_mod_eq_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b x : α} (hb : 0 < b) :
to_Ico_mod a hb x = x x set.Ico a (a + b)
theorem to_Ioc_mod_eq_self {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b x : α} (hb : 0 < b) :
to_Ioc_mod a hb x = x x set.Ioc a (a + b)
@[simp]
theorem to_Ico_mod_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a₁ a₂ : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a₁ hb (to_Ico_mod a₂ hb x) = to_Ico_mod a₁ hb x
@[simp]
theorem to_Ico_mod_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a₁ a₂ : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a₁ hb (to_Ioc_mod a₂ hb x) = to_Ico_mod a₁ hb x
@[simp]
theorem to_Ioc_mod_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a₁ a₂ : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a₁ hb (to_Ioc_mod a₂ hb x) = to_Ioc_mod a₁ hb x
@[simp]
theorem to_Ioc_mod_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a₁ a₂ : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a₁ hb (to_Ico_mod a₂ hb x) = to_Ioc_mod a₁ hb x
theorem to_Ico_mod_periodic {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
theorem to_Ioc_mod_periodic {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
@[simp]
theorem quotient_add_group.equiv_Ico_mod_symm_apply {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (ᾰ : (set.Ico a (a + b))) :
noncomputable def quotient_add_group.equiv_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :

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 α] (a : α) {b : α} (hb : 0 < b) (x : α) :
noncomputable def quotient_add_group.equiv_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :

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 α] (a : α) {b : α} (hb : 0 < b) (ᾰ : (set.Ioc a (a + b))) :
@[simp]
theorem quotient_add_group.equiv_Ioc_mod_coe {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
theorem to_Ico_div_eq_floor {α : Type u_1} [linear_ordered_field α] [floor_ring α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb x = (x - a) / b
theorem to_Ioc_div_eq_neg_floor {α : Type u_1} [linear_ordered_field α] [floor_ring α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb x = -(a + b - x) / b
theorem to_Ico_mod_eq_add_fract_mul {α : Type u_1} [linear_ordered_field α] [floor_ring α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb x = a + int.fract ((x - a) / b) * b
theorem to_Ico_mod_eq_fract_mul {α : Type u_1} [linear_ordered_field α] [floor_ring α] {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod 0 hb x = int.fract (x / b) * b
theorem to_Ioc_mod_eq_sub_fract_mul {α : Type u_1} [linear_ordered_field α] [floor_ring α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb x = a + b - int.fract ((a + b - x) / b) * b