exists_succ_get?_stream_of_gcf_of_get?_eq_some

English

If the nth stream equals some ifp_succ, then the nth tail of the head sequence has a specific form: (of v).s.get? n = Some{a=1, b=ifp_succ.b.cast}.

Русский

Если поток на позиции n равен определённому ifp_succ, то хвост головы имеет вид Some(⟨1, ifp_succ.b.cast⟩).

LaTeX

$$$\text{If } \operatorname{IntFractPair}.\operatorname{stream}(v,n+1) = \mathrm{Some}(ifp_{succ}) \text{ then } (\operatorname GenContFract.of}(v)).s.get?\,n = \mathrm{Some} \langle 1, ifp_{succ}.b.cast \rangle$$$

Lean4

theorem exists_succ_get?_stream_of_gcf_of_get?_eq_some {gp_n : Pair K} (s_nth_eq : (of v).s.get? n = some gp_n) :
    ∃ ifp : IntFractPair K, IntFractPair.stream v (n + 1) = some ifp ∧ (ifp.b : K) = gp_n.b :=
  by
  obtain ⟨ifp, stream_succ_nth_eq, gp_n_eq⟩ :
    ∃ ifp, IntFractPair.stream v (n + 1) = some ifp ∧ Pair.mk 1 (ifp.b : K) = gp_n :=
    by
    unfold of IntFractPair.seq1 at s_nth_eq
    simpa [Stream'.Seq.get?_tail, Stream'.Seq.map_get?] using s_nth_eq
  cases gp_n_eq
  simp_all only [Option.some.injEq, exists_eq_left']

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