convergent_succ — Mathlib

English

The (n+1)th convergent of ξ equals ⌊ξ⌋ plus the inverse of the nth convergent of fract ξ.

Русский

(n+1)-й конвергент ξ равен ⌊ξ⌋ плюс обратная к n-му конвергенту дробной части ξ.

LaTeX

$$$$\\xi.convergent(n+1) = \\lfloor\\xi\\rfloor + (\\operatorname{fract}(\\xi)^{-1}.convergent n)^{-1}.$$$$

Lean4

/-- The `(n+1)`th convergent of `ξ` is the `n`th convergent of `1/(fract ξ)`. -/
@[simp]
theorem convergent_succ (ξ : ℝ) (n : ℕ) : ξ.convergent (n + 1) = ⌊ξ⌋ + ((fract ξ)⁻¹.convergent n)⁻¹ :=
  rfl

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