AbsoluteValue.exists_partition_int

theorem AbsoluteValue.exists_partition_int : ∀ (n : ℕ) {ε : ℝ}, 0 < ε → ∀ {b : ℤ}, b ≠ 0 → ∀ (A : Fin n → ℤ), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε

This theorem states that for any positive real number ε, any non-zero integer b, and any function A from the finite set of natural numbers less than n to the integers, there exists a function t such that for any two elements in the finite set, if they are mapped to the same value by function t, the absolute difference of their remainders when divided by b (when these elements are mapped by function A) is less than b times ε.

More concisely: Given any positive real number ε, integer b != 0, and function A from {0..n-1} to ℤ, there exists a function t such that |A(i) % b - A(j) % b| < εβ for all i, j with t(i) = t(j).