convs_eq_convergent — Mathlib

English

The nth convergent of GenContFract.of ξ equals ξ.convergent n (as real to rational embedding).

Русский

N-й конвергент GenContFract.of ξ совпадает с ξ.convergent n (с встраиванием в рациональные).

LaTeX

$$$$ (\\mathrm{GenContFract}.of \\xi).convs n = \\xi.convergent n.$$$$

Lean4

/-- The `n`th convergent of the `GenContFract.of ξ` agrees with `ξ.convergent n`. -/
theorem convs_eq_convergent (ξ : ℝ) (n : ℕ) : (GenContFract.of ξ).convs n = ξ.convergent n := by
  induction n generalizing ξ with
  | zero => simp only [zeroth_conv_eq_h, of_h_eq_floor, convergent_zero, Rat.cast_intCast]
  | succ n ih => rw [convs_succ, ih (fract ξ)⁻¹, convergent_succ, one_div]; norm_cast

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