conts_stable_of_terminated — Mathlib

English

Let g be a generalized continued fraction over a division ring K. If it terminates at stage n and n ≤ m, then the conts at stage m equals the conts at stage n.

Русский

Пусть g — обобщённая непрерывная дробь над делением кольца K. Если завершение дроби происходит на шаге n и выполняется n ≤ m, то conts на шаге m совпадает с conts на шаге n.

LaTeX

$$$\\\\forall K \\, g \\; (n,m) \in \\mathbb{N}^2 \\, (n \\le m) \\, (g.TerminatedAt n) \\Rightarrow g.conts m = g.conts n$$$

Lean4

theorem conts_stable_of_terminated (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) : g.conts m = g.conts n := by
  simp only [nth_cont_eq_succ_nth_contAux, contsAux_stable_of_terminated (Nat.pred_le_iff.mp n_le_m) terminatedAt_n]

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