convs'_stable_of_terminated — Mathlib

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]

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