English
Let R be a Euclidean domain and S a domain equipped with a basis bS and an admissible absolute value abv. Then an element x of R lies in the finite set finsetApprox(bS, adm) exactly when x can be written as the difference of two distinct basis elements, i.e. x = distinctElems(bS, adm, i) − distinctElems(bS, adm, j) with i ≠ j.
Русский
Пусть R — евклидово домено, а S — домен с базисом bS и допустимой абсолютной величиной abv. Тогда элемент x ∈ R принадлежит конечному множеству finsetApprox(bS, adm) тогда и только тогда существует пара индексов i ≠ j such that x = distinctElems(bS, adm, i) − distinctElems(bS, adm, j).
LaTeX
$$$ x \\in \\mathrm{finsetApprox}(b_S, \\mathrm{adm}) \\iff \\exists i,j,\\ i \\neq j \\land \\operatorname{distinctElems}(b_S, \\mathrm{adm}, i) - \\operatorname{distinctElems}(b_S, \\mathrm{adm}, j) = x $$$
Lean4
@[simp]
theorem mem_finsetApprox {x : R} :
x ∈ finsetApprox bS adm ↔ ∃ i j, i ≠ j ∧ distinctElems bS adm i - distinctElems bS adm j = x :=
by
simp only [finsetApprox, Finset.mem_erase, Finset.mem_image]
constructor
· rintro ⟨hx, ⟨i, j⟩, _, rfl⟩
refine ⟨i, j, ?_, rfl⟩
rintro rfl
simp at hx
· rintro ⟨i, j, hij, rfl⟩
refine ⟨?_, ⟨i, j⟩, Finset.mem_univ _, rfl⟩
rw [Ne, sub_eq_zero]
exact fun h => hij ((distinctElems bS adm).injective h)
