le_of_succ_succ_get?_contsAux_b — Mathlib

English

The partial numerators a_i are equal to 1.

Русский

Частные числители a_i равны 1.

LaTeX

$$$\\\\forall {a : K} (nth_partNum_eq : (of v).partNums.get? n = Some a) \\\\Rightarrow a = 1$$$

Lean4

theorem le_of_succ_succ_get?_contsAux_b {b : K} (nth_partDen_eq : (of v).partDens.get? n = some b) :
    b * ((of v).contsAux <| n + 1).b ≤ ((of v).contsAux <| n + 2).b :=
  by
  obtain ⟨gp_n, nth_s_eq, rfl⟩ : ∃ gp_n, (of v).s.get? n = some gp_n ∧ gp_n.b = b :=
    exists_s_b_of_partDen nth_partDen_eq
  simp [of_partNum_eq_one (partNum_eq_s_a nth_s_eq), zero_le_of_contsAux_b,
    GenContFract.contsAux_recurrence nth_s_eq rfl rfl]

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