partNum_eq_s_a — Mathlib

English

If the nth term of s is gp, then the nth part number is some gp.a.

Русский

Если n-й элемент последовательности s равен gp, тогда n-й номер части равен some gp.a.

LaTeX

$$$$ \forall {gp : GenContFract.Pair(\alpha)}, \ g.s.get? n = \text{some } gp \Rightarrow g.partNums.get? n = \text{some } gp.a. $$$$

Lean4

theorem partNum_eq_s_a {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) : g.partNums.get? n = some gp.a := by
  simp [partNums, s_nth_eq]

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