get?_seq1_eq_succ_get?_stream — Mathlib

English

The snd component of Seq1 v evaluated at n, get? n, equals the (n+1)th stream term of v: (IntFractPair.seq1 v).snd.get? n = IntFractPair.stream v (n+1).

Русский

Второй компонент Seq1(v) на позиции n равен (n+1)-му члену потока IntFractPair.

LaTeX

$$$((\operatorname{IntFractPair}.\operatorname{seq1}(v)).\operatorname{snd}).get?\,n = \operatorname{IntFractPair}.\operatorname{stream}(v, n+1)$$$

Lean4

theorem get?_seq1_eq_succ_get?_stream : (IntFractPair.seq1 v).snd.get? n = (IntFractPair.stream v) (n + 1) :=
  rfl

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