first_cont_eq — Mathlib

English

If the zeroth state is gp, then the first conts equals ⟨gp.b · h + gp.a, gp.b⟩.

Русский

Если нулевое состояние равно gp, то первый элемент conts равен ⟨gp.b · h + gp.a, gp.b⟩.

LaTeX

$$$ g.conts 1 = \\langle gp.b \\cdot g.h + gp.a, gp.b \\rangle \\quad$ при $g.s.get? 0 = \\text{some } gp$$$

Lean4

theorem first_cont_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) : g.conts 1 = ⟨gp.b * g.h + gp.a, gp.b⟩ := by
  simp [nth_cont_eq_succ_nth_contAux, second_contAux_eq zeroth_s_eq]

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