stream_succ_of_int — Mathlib

English

For any IsStrictOrderedRing K, the stream of an integer a in K terminates after the first term: the (n+1)th term is none for all n.

Русский

Для любого IsStrictOrderedRing K поток целого числа a в K прекращается после первого члена: для всех n следующий член равен none.

LaTeX

$$$\forall a\in\mathbb{Z},\;\operatorname{IntFractPair}.\operatorname{stream}(a:K,n+1) = \mathrm{None}$$$

Lean4

/-- The stream of `IntFractPair`s of an integer stops after the first term.
-/
theorem stream_succ_of_int [IsStrictOrderedRing K] (a : ℤ) (n : ℕ) : IntFractPair.stream (a : K) (n + 1) = none := by
  induction n with
  | zero =>
    refine IntFractPair.stream_eq_none_of_fr_eq_zero (IntFractPair.stream_zero (a : K)) ?_
    simp only [IntFractPair.of, Int.fract_intCast]
  | succ n ih => exact IntFractPair.succ_nth_stream_eq_none_iff.mpr (Or.inl ih)

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