nums_stable_of_terminated — Mathlib

English

Let g be a generalized continued fraction over a division ring K. If g terminates at n and n ≤ m, then g.nums m = g.nums n.

Русский

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

LaTeX

$$$$ \forall K, \forall g : GenContFract(K), \forall n,m \in \mathbb{N},\; (n \le m \land g.TerminatedAt n) \Rightarrow g.nums m = g.nums n. $$$$

Lean4

theorem nums_stable_of_terminated (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) : g.nums m = g.nums n := by
  simp only [num_eq_conts_a, conts_stable_of_terminated n_le_m terminatedAt_n]

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