squashSeq_nth_of_lt — Mathlib

English

The auxiliary convergents convs'Aux stay aligned with the squashed sequence: convs'Aux s (n+2) = convs'Aux (squashSeq s n) (n+1).

Русский

Вспомогательные равенства сходящихся последовательностей convs'Aux остаются согласованными с схлопнутой последовательностью: convs'Aux s (n+2) = convs'Aux (squashSeq s n) (n+1).

LaTeX

$$$\text{convs'Aux}(s,n+2) = \text{convs'Aux}(\text{squashSeq}(s,n),n+1).$$$

Lean4

/-- The values before the squashed position stay the same. -/
theorem squashSeq_nth_of_lt {m : ℕ} (m_lt_n : m < n) : (squashSeq s n).get? m = s.get? m := by
  cases s_succ_nth_eq : s.get? (n + 1) with
  | none => rw [squashSeq_eq_self_of_terminated s_succ_nth_eq]
  | some =>
    obtain ⟨gp_n, s_nth_eq⟩ : ∃ gp_n, s.get? n = some gp_n := s.ge_stable n.le_succ s_succ_nth_eq
    simp [*, squashSeq, m_lt_n.ne]

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