le_of_succ_get?_den — Mathlib

English

There exists an integer z such that b = z for the nth partDen.

Русский

Существование целого z: b = z на позиции nth partDen.

LaTeX

$$$\\\\forall {b : K} (nth_partDen_eq : (of v).partDens.get? n = Some b), \\\\exists z : \\\\mathbb{Z}, b = (z : K)$$$

Lean4

/-- Shows that `bₙ * Bₙ ≤ Bₙ₊₁`, where `bₙ` is the `n`th partial denominator and `Bₙ₊₁` and `Bₙ` are
the `n + 1`th and `n`th denominator of the continued fraction. -/
theorem le_of_succ_get?_den {b : K} (nth_partDenom_eq : (of v).partDens.get? n = some b) :
    b * (of v).dens n ≤ (of v).dens (n + 1) :=
  by
  rw [den_eq_conts_b, nth_cont_eq_succ_nth_contAux]
  exact le_of_succ_succ_get?_contsAux_b nth_partDenom_eq

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