of_terminatedAt_iff_intFractPair_seq1_terminatedAt

English

If the nth tail of the head sequence equals some gp_n, then there exists a next pair ifp with the (n+1)th stream equal to some ifp and whose b-component, after casting, matches gp_n.b.

Русский

Если n-й хвост головы равен некоторому gp_n, существует следующий элемент ifp так, что поток на позиции n+1 равен Some ifp и b-коэффициент после приведения совпадает с gp_n.b.

LaTeX

$$$\text{If } (\operatorname GenContFract.of(v)).s.get?\,n = \mathrm{Some}(gp_n)\;\text{ then }\; \exists ifp,\; \operatorname{IntFractPair}.\operatorname{stream}(v,n+1) = \mathrm{Some}(ifp) \land ifp.b.cast = gp_n.b$$$

Lean4

theorem of_terminatedAt_iff_intFractPair_seq1_terminatedAt :
    (of v).TerminatedAt n ↔ (IntFractPair.seq1 v).snd.TerminatedAt n :=
  Option.map_eq_none_iff

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