contsAux_recurrence — Mathlib

English

Recurrence for contsAux generalizes to g.contsAux (n+2) as function of gp, pred, ppred.

Русский

Рекуррентность contsAux обобщается на contsAux(n+2) как функция от gp, pred, ppred.

LaTeX

$$$g.contsAux(n+2) = \langle gp.b \cdot pred.a + gp.a \cdot ppred.a, gp.b \cdot pred.b + gp.a \cdot ppred.b \rangle$$$

Lean4

theorem contsAux_recurrence {gp ppred pred : Pair K} (nth_s_eq : g.s.get? n = some gp)
    (nth_contsAux_eq : g.contsAux n = ppred) (succ_nth_contsAux_eq : g.contsAux (n + 1) = pred) :
    g.contsAux (n + 2) = ⟨gp.b * pred.a + gp.a * ppred.a, gp.b * pred.b + gp.a * ppred.b⟩ := by
  simp [*, contsAux, nextConts, nextDen, nextNum]

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