coe_stream'_rat_eq — Mathlib

English

The rat-augmented stream equality transfers to the standard stream equality via the Stream' construction.

Русский

Существование эквивалентности потоков в обобщённой структуре постепенно переходит к обычной равенству потоков через конструкт Stream'.

LaTeX

$$$\\text{Stream'}\\text{.Eq}((IntFractPair.stream q), v) \\Rightarrow \\text{Stream'}.Eq(\\text{IntFractPair.stream} v)$$$

Lean4

theorem coe_stream'_rat_eq (v_eq_q : v = (↑q : K)) :
    ((IntFractPair.stream q).map (Option.map (mapFr (↑))) : Stream' <| Option <| IntFractPair K) =
      IntFractPair.stream v :=
  by funext n; exact IntFractPair.coe_stream_nth_rat_eq v_eq_q n

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