partDen_eq_s_b — Mathlib

English

If the nth term of s is gp, then the nth part denominator is gp.b.

Русский

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

LaTeX

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

Lean4

theorem partDen_eq_s_b {gp : Pair α} (s_nth_eq : g.s.get? n = some gp) : g.partDens.get? n = some gp.b := by
  simp [partDens, s_nth_eq]

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