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 #
to_Ico_div hp a b(wherehp : 0 < p): The unique integer such that this multiple ofp, subtracted fromb, is inIco a (a + p).to_Ico_mod hp a b(wherehp : 0 < p): Reducebto the intervalIco a (a + p).to_Ioc_div hp a b(wherehp : 0 < p): The unique integer such that this multiple ofp, subtracted fromb, is inIoc a (a + p).to_Ioc_mod hp a b(wherehp : 0 < p): Reducebto the intervalIoc a (a + p).
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
- to_Ico_div hp a b = Exists.some _
theorem
sub_to_Ico_div_zsmul_mem_Ico
{α : Type u_1}
[linear_ordered_add_comm_group α]
[hα : archimedean α]
{p : α}
(hp : 0 < p)
(a b : α) :
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
- to_Ioc_div hp a b = Exists.some _
theorem
sub_to_Ioc_div_zsmul_mem_Ioc
{α : Type u_1}
[linear_ordered_add_comm_group α]
[hα : archimedean α]
{p : α}
(hp : 0 < p)
(a b : α) :
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
- to_Ico_mod hp a b = b - to_Ico_div hp a b • p
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
- to_Ioc_mod hp a b = b - to_Ioc_div hp a b • p
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 : α) :
to_Ico_mod hp 0 b ∈ set.Ico 0 p
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 : α} :
theorem
to_Ioc_mod_eq_iff
{α : Type u_1}
[linear_ordered_add_comm_group α]
[hα : archimedean α]
{p : α}
(hp : 0 < p)
{a b c : α} :
@[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
Links between the Ico and Ioc variants applied to the same element #
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 : α} :
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 : α} :
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 : α} :
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 : α} :
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_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 : α} :
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 : α} :
theorem
to_Ioc_mod_eq_self
{α : Type u_1}
[linear_ordered_add_comm_group α]
[hα : archimedean α]
{p : α}
(hp : 0 < p)
{a b : α} :
@[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 : α) :
function.periodic (to_Ico_mod hp a) p
theorem
to_Ioc_mod_periodic
{α : Type u_1}
[linear_ordered_add_comm_group α]
[hα : archimedean α]
{p : α}
(hp : 0 < p)
(a : α) :
function.periodic (to_Ioc_mod hp a) p
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))) :
⇑((quotient_add_group.equiv_Ico_mod hp a).symm) ᾰ = ↑ᾰ
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
- quotient_add_group.equiv_Ico_mod hp a = {to_fun := λ (b : α ⧸ add_subgroup.zmultiples p), ⟨_.lift b, _⟩, inv_fun := coe coe_to_lift, left_inv := _, right_inv := _}
@[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 : α) :
⇑(quotient_add_group.equiv_Ico_mod hp a) ↑b = ⟨to_Ico_mod hp 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 : α) :
⇑(quotient_add_group.equiv_Ico_mod hp a) 0 = ⟨to_Ico_mod hp a 0, _⟩
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
- quotient_add_group.equiv_Ioc_mod hp a = {to_fun := λ (b : α ⧸ add_subgroup.zmultiples p), ⟨_.lift b, _⟩, inv_fun := coe coe_to_lift, left_inv := _, right_inv := _}
@[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))) :
⇑((quotient_add_group.equiv_Ioc_mod hp a).symm) ᾰ = ↑ᾰ
@[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 : α) :
⇑(quotient_add_group.equiv_Ioc_mod hp a) ↑b = ⟨to_Ioc_mod hp 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 : α) :
⇑(quotient_add_group.equiv_Ioc_mod hp a) 0 = ⟨to_Ioc_mod hp a 0, _⟩
The circular order structure on α ⧸ add_subgroup.zmultiples p #
@[protected, instance]
def
quotient_add_group.has_quotient.quotient.has_btw
{α : Type u_1}
[linear_ordered_add_comm_group α]
[hα : archimedean α]
{p : α}
[hp' : fact (0 < p)] :
has_btw (α ⧸ add_subgroup.zmultiples p)
Equations
- quotient_add_group.has_quotient.quotient.has_btw = {btw := λ (x₁ x₂ x₃ : α ⧸ add_subgroup.zmultiples p), ↑(⇑(quotient_add_group.equiv_Ico_mod quotient_add_group.has_quotient.quotient.has_btw._proof_1 0) (x₂ - x₁)) ≤ ↑(⇑(quotient_add_group.equiv_Ioc_mod quotient_add_group.has_quotient.quotient.has_btw._proof_3 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 _ 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₃
@[protected, instance]
def
quotient_add_group.circular_preorder
{α : Type u_1}
[linear_ordered_add_comm_group α]
[hα : archimedean α]
{p : α}
[hp' : fact (0 < p)] :
Equations
- quotient_add_group.circular_preorder = {to_has_btw := quotient_add_group.has_quotient.quotient.has_btw hp', to_has_sbtw := {sbtw := λ (_x _x_1 _x_2 : α ⧸ add_subgroup.zmultiples p), has_btw.btw _x _x_1 _x_2 ∧ ¬has_btw.btw _x_2 _x_1 _x}, btw_refl := _, btw_cyclic_left := _, sbtw_iff_btw_not_btw := _, sbtw_trans_left := _}
@[protected, instance]
def
quotient_add_group.circular_order
{α : Type u_1}
[linear_ordered_add_comm_group α]
[hα : archimedean α]
{p : α}
[hp' : fact (0 < p)] :
Equations
- quotient_add_group.circular_order = {to_circular_partial_order := {to_circular_preorder := {to_has_btw := circular_preorder.to_has_btw quotient_add_group.circular_preorder, to_has_sbtw := circular_preorder.to_has_sbtw quotient_add_group.circular_preorder, btw_refl := _, btw_cyclic_left := _, sbtw_iff_btw_not_btw := _, sbtw_trans_left := _}, btw_antisymm := _}, btw_total := _}
theorem
to_Ico_div_eq_floor
{α : Type u_1}
[linear_ordered_field α]
[floor_ring α]
{p : α}
(hp : 0 < p)
(a b : α) :
theorem
to_Ioc_div_eq_neg_floor
{α : Type u_1}
[linear_ordered_field α]
[floor_ring α]
{p : α}
(hp : 0 < p)
(a b : α) :
theorem
to_Ico_div_zero_one
{α : Type u_1}
[linear_ordered_field α]
[floor_ring α]
(b : α) :
to_Ico_div _ 0 b = ⌊b⌋
theorem
to_Ico_mod_eq_add_fract_mul
{α : Type u_1}
[linear_ordered_field α]
[floor_ring α]
{p : α}
(hp : 0 < p)
(a b : α) :
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 : α) :
theorem
to_Ico_mod_zero_one
{α : Type u_1}
[linear_ordered_field α]
[floor_ring α]
(b : α) :
to_Ico_mod _ 0 b = int.fract b
Lemmas about unions of translates of intervals #
theorem
Union_Ioc_zsmul
{α : Type u_1}
[linear_ordered_add_comm_group α]
[archimedean α]
{p : α}
(hp : 0 < p) :
theorem
Union_Ico_zsmul
{α : Type u_1}
[linear_ordered_add_comm_group α]
[archimedean α]
{p : α}
(hp : 0 < p) :
theorem
Union_Icc_zsmul
{α : Type u_1}
[linear_ordered_add_comm_group α]
[archimedean α]
{p : α}
(hp : 0 < p) :