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 #

source
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
source
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)
source
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
source
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
source
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)
source
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
source
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
source
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
source
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)
source
theorem to_Ico_mod_mem_Ico' {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod 0 hb x ∈ set.Ico 0 b
source
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)
source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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)
source
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)
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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 : α} :
¬mem_Ioo_mod a b x ↔ ↑x = ↑a
source
theorem mem_Ioo_mod_iff_ne_mod_zmultiples {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] {a b : α} (hb : 0 < b) {x : α} :
mem_Ioo_mod a b x ↔ ↑x ≠ ↑a
source
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)
source
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
source
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
source
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
source
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)
source
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)
source
@[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
source
@[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
source
@[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
source
@[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
source
theorem to_Ico_mod_periodic {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
function.periodic (to_Ico_mod a hb) b
source
theorem to_Ioc_mod_periodic {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
function.periodic (to_Ioc_mod a hb) b
source
@[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))) :
⇑((quotient_add_group.equiv_Ico_mod a hb).symm) ᾰ = ↑ᾰ
source
noncomputable def quotient_add_group.equiv_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
α ⧸ add_subgroup.zmultiples b ≃ ↥(set.Ico a (a + b))

to_Ico_mod as an equiv from the quotient.

Equations
source
@[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 : α) :
⇑(quotient_add_group.equiv_Ico_mod a hb) ↑x = ⟨to_Ico_mod a hb x, _⟩
source
noncomputable def quotient_add_group.equiv_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [hα : archimedean α] (a : α) {b : α} (hb : 0 < b) :
α ⧸ add_subgroup.zmultiples b ≃ ↥(set.Ioc a (a + b))

to_Ioc_mod as an equiv from the quotient.

Equations
source
@[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))) :
⇑((quotient_add_group.equiv_Ioc_mod a hb).symm) ᾰ = ↑ᾰ
source
@[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 : α) :
⇑(quotient_add_group.equiv_Ioc_mod a hb) ↑x = ⟨to_Ioc_mod a hb x, _⟩
source
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⌋
source
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⌋
source
theorem to_Ico_div_zero_one {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) :
to_Ico_div 0 zero_lt_one x = ⌊x⌋
source
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
source
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
source
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
source
theorem to_Ico_mod_zero_one {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) :
to_Ico_mod 0 zero_lt_one x = int.fract x