get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero

English

If the nth tail s.get? n equals some gp_n, then there exists ifp such that IntFractPair.stream v (n+1) = some ifp and ifp.b.cast gp_n.b.

Русский

Если n-й хвост равен некоторому gp_n, существует ifp такой, что поток на n+1 равен some ifp и ifp.b.cast совпадает с gp_n.b.

LaTeX

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

Lean4

/-- Shows how the entries of the sequence of the computed continued fraction can be obtained by the
fractional parts of the stream of integer and fractional parts.
-/
theorem get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero {ifp_n : IntFractPair K}
    (stream_nth_eq : IntFractPair.stream v n = some ifp_n) (nth_fr_ne_zero : ifp_n.fr ≠ 0) :
    (of v).s.get? n = some ⟨1, (IntFractPair.of ifp_n.fr⁻¹).b⟩ :=
  get?_of_eq_some_of_succ_get?_intFractPair_stream <| IntFractPair.stream_succ_of_some stream_nth_eq nth_fr_ne_zero

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