stream_isSeq — Mathlib

English

The IntFractPair.stream sequence has the IsSeq property: if at some n we get none, then at n+1 we also get none.

Русский

Поток IntFractPair.stream имеет свойство IsSeq: если на позиции n получаем none, то на n+1 также получаем none.

LaTeX

$$$\\\\forall {K} [DivisionRing K] [LinearOrder K] [FloorRing K] (v : K), (IntFractPair.stream v).IsSeq$$$

Lean4

/-- Shows that `IntFractPair.stream` has the sequence property, that is once we return `none` at
position `n`, we also return `none` at `n + 1`.
-/
theorem stream_isSeq (v : K) : (IntFractPair.stream v).IsSeq :=
  by
  intro _ hyp
  simp [IntFractPair.stream, hyp]

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