GeneralizedContinuedFraction.IntFractPair.stream_isSeq

theorem GeneralizedContinuedFraction.IntFractPair.stream_isSeq : ∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] (v : K), (GeneralizedContinuedFraction.IntFractPair.stream v).IsSeq

This theorem states that for any linearly ordered field `K` that also has the structure of a floor ring, the function `GeneralizedContinuedFraction.IntFractPair.stream` applied to any element `v` of `K`, produces a sequence in the sense defined by `Stream'.IsSeq`. That is, if for some natural number `n`, the `n`-th element of the stream is `none`, then the `(n + 1)`-th element is also `none`. In other words, once the stream returns `none`, it will continue to do so for all subsequent indices.

More concisely: For any linearly ordered field `K` that is also a floor ring, the sequence produced by `GeneralizedContinuedFraction.IntFractPair.stream` on any element `v` of `K` is a stream in the sense of `Stream'.IsSeq`, meaning that if the `n`-th element is `none`, then all subsequent elements are also `none`.