English
For δ: ℕ → ℝ and x in the unit circle, membership of x in approxAddOrderOf(UnitAddCircle, n, δ) is equivalent to the existence of m < n with gcd(m,n) = 1 and |x − m/n| < δ(n).
Русский
Для δ: ℕ → ℝ и x ∈ единичной окружности, членство x в approxAddOrderOf(UnitAddCircle, n, δ) эквивалентно существованию m < n с gcd(m,n) = 1 и |x − m/n| < δ(n).
LaTeX
$$$$ x \\in \\operatorname{approxAddOrderOf}(\\text{UnitAddCircle}, n, δ) \\iff \\exists m < n, \\gcd(m,n) = 1 \\land \\|x - \\frac{m}{n}\\| < δ. $$$$
Lean4
theorem mem_approxAddOrderOf_iff {δ : ℝ} {x : UnitAddCircle} {n : ℕ} (hn : 0 < n) :
x ∈ approxAddOrderOf UnitAddCircle n δ ↔ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑((m : ℝ) / n)‖ < δ :=
by
simp only [mem_approx_add_orderOf_iff, mem_setOf_eq, ball, dist_eq_norm, AddCircle.addOrderOf_eq_pos_iff hn, mul_one]
constructor
· rintro ⟨y, ⟨m, hm₁, hm₂, rfl⟩, hx⟩; exact ⟨m, hm₁, hm₂, hx⟩
· rintro ⟨m, hm₁, hm₂, hx⟩; exact ⟨↑((m : ℝ) / n), ⟨m, hm₁, hm₂, rfl⟩, hx⟩
