English
Let g be a generalized continued fraction over a division ring K. If g terminates at n, then for all m ≥ n, g.convs' m = g.convs' n.
Русский
Пусть g — обобщённое продолженное дробление над кольцом деления K. Если g завершается в позиции n, то для всех m ≥ n выполняется g.convs' m = g.convs' n.
LaTeX
$$$$ \forall K, \forall g : GenContFract(K), \forall n,m \in \mathbb{N},\; (n \le m \land g.TerminatedAt n) \Rightarrow g.convs' m = g.convs' n. $$$$
Lean4
theorem convs'_stable_of_terminated (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) : g.convs' m = g.convs' n := by
simp only [convs', convs'Aux_stable_of_terminated n_le_m terminatedAt_n]