dens_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.dens m = g.dens n.

Русский

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

LaTeX

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

Lean4

theorem dens_stable_of_terminated (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) : g.dens m = g.dens n := by
  simp only [den_eq_conts_b, conts_stable_of_terminated n_le_m terminatedAt_n]

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