Ass — Mathlib

English

A technical version: from Legendre's approximation, there exists n with a rational equal to ξ.convergent n when certain coprimality and inequality conditions hold.

Русский

Техническая версия Лежандра: при выполнении условий на пары чисел и копротности существует n, для которого q = ξ.convergent n.

LaTeX

$$$$\\exists n\\; (u/v)=\\xi.convergent n \\quad\\text{under suitable Legendre conditions.}$$$$

Lean4

/-- Define the technical condition to be used as assumption in the inductive proof. -/
def Ass (ξ : ℝ) (u v : ℤ) : Prop :=
  IsCoprime u v ∧
    (v = 1 → (-(1 / 2) : ℝ) < ξ - u) ∧
      |ξ - u / v| <
        ((v : ℝ) * (2 * v - 1))⁻¹
          -- ### Auxiliary lemmas
          -- This saves a few lines below, as it is frequently needed.

Похожие утверждения