convs'Aux_stable_of_terminated — Mathlib

English

If n ≤ m and the sequence terminates at n, convs'Aux s m = convs'Aux s n, showing stability of the auxiliary convergents.

Русский

Если n ≤ m и последовательность завершается на n, то convs'Aux s m = convs'Aux s n, что демонстрирует устойчивость вспомогательных сходящихся дробей.

LaTeX

$$$n \\le m \\land s. TerminatedAt\\ n \\Rightarrow convs'Aux\; s\ m = convs'Aux\; s\ n$$$

Lean4

theorem convs'Aux_stable_of_terminated {s : Stream'.Seq <| Pair K} (n_le_m : n ≤ m)
    (terminatedAt_n : s.TerminatedAt n) : convs'Aux s m = convs'Aux s n := by
  induction n_le_m with
  | refl => rfl
  | step n_le_m IH =>
    refine (convs'Aux_stable_step_of_terminated (?_)).trans IH
    exact s.terminated_stable n_le_m terminatedAt_n

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