convs'Aux_succ_some — Mathlib

English

If the head of s is some p, then convs'Aux s (n+1) equals p.a / (p.b + convs'Aux s.tail n).

Русский

Если голова последовательности пуста не пуста, то convs'Aux s (n+1) = p.a / (p.b + convs'Aux s.tail n).

LaTeX

$$$ s.head = \\text{some } p \\Rightarrow \\ convs'Aux\\, s\\ (n+1) = \\ frac{p.a}{p.b + convs'Aux\\, s.tail\\, n} $$$

Lean4

theorem convs'Aux_succ_some {s : Stream'.Seq (Pair K)} {p : Pair K} (h : s.head = some p) (n : ℕ) :
    convs'Aux s (n + 1) = p.a / (p.b + convs'Aux s.tail n) := by simp [convs'Aux, h]

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