of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none

English

Termination of the head continued fraction after n steps is equivalent to termination of the second component of the nth term of the sequence (seq1 v).snd at n.

Русский

Прекращение головной цепной дроби через n шагов эквивалентно прекращению второго компонента пары в последовательности на позиции n.

LaTeX

$$$(\operatorname GenContFract.of(v)).TerminatedAt n \iff (\operatorname{IntFractPair.seq1}(v).snd).TerminatedAt n$$$

Lean4

theorem of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none :
    (of v).TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none := by
  rw [of_terminatedAt_iff_intFractPair_seq1_terminatedAt, Stream'.Seq.TerminatedAt,
    IntFractPair.get?_seq1_eq_succ_get?_stream]

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