get?_of_eq_some_of_succ_get?_intFractPair_stream

English

The nth head term of the original sequence can be obtained from the successor terms: (of v).s.get? (n+1) equals (of (fract v)^{-1}).s.get? n.

Русский

(n+1)-й член головы можно выразить через следующий: (of v).s.get? (n+1) = (of (fract v)^{-1}).s.get? n.

LaTeX

$$$\forall n,\; (\operatorname GenContFract.of}(v)).s.get? (n+1) = (\operatorname GenContFract.of}(\operatorname{fract}(v)^{-1})).s.get? n$$$

Lean4

/-- Shows how the entries of the sequence of the computed continued fraction can be obtained by the
integer parts of the stream of integer and fractional parts.
-/
theorem get?_of_eq_some_of_succ_get?_intFractPair_stream {ifp_succ_n : IntFractPair K}
    (stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n) : (of v).s.get? n = some ⟨1, ifp_succ_n.b⟩ :=
  by
  unfold of IntFractPair.seq1
  simp [Stream'.Seq.map_tail, Stream'.Seq.get?_tail, Stream'.Seq.map_get?, stream_succ_nth_eq]

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