English
For a Euclidean domain R and an admissible abv, there exists a partition of a finite family of elements modulo b with a closeness property.
Русский
Для евклидова домена R и допустимой abv существует разбиение конечной семейства элементов по модулю b с близостью.
LaTeX
$$$\exists t : ι \to Fin (h.card ε),\; \forall i_0,i_1, t i_0 = t i_1 \Rightarrow (abv (A i_1 - A i_0) : \mathbb{R}) < abv(b) \cdot ε$$$
Lean4
/-- For all `ε > 0` and finite families `A`, we can partition the remainders of `A` mod `b`
into `abv.card ε` sets, such that all elements in each part of remainders are close together. -/
theorem exists_partition {ι : Type*} [Finite ι] {ε : ℝ} (hε : 0 < ε) {b : R} (hb : b ≠ 0) (A : ι → R)
(h : abv.IsAdmissible) :
∃ t : ι → Fin (h.card ε), ∀ i₀ i₁, t i₀ = t i₁ → (abv (A i₁ % b - A i₀ % b) : ℝ) < abv b • ε :=
by
rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
obtain ⟨t, ht⟩ := h.exists_partition' n hε hb (A ∘ e.symm)
refine ⟨t ∘ e, fun i₀ i₁ h ↦ ?_⟩
convert (config := { transparency := .default }) ht (e i₀) (e i₁) h <;> simp only [e.symm_apply_apply]
