of_correctness_of_terminates — Mathlib

English

If GenContFract.of v terminates, there exists n such that v equals the nth convergent: ∃ n, v = (of v).convs n.

Русский

Если GenContFract.of v завершается, существует n, такой что v = (of v).convs n.

LaTeX

$$$(\\mathrm{Terminates}) \\rightarrow \\exists n:\\mathbb{N},\\ v = (\\mathrm{of}\\, v).convs n$$$

Lean4

/-- If `GenContFract.of v` terminates, then there is `n : ℕ` such that the `n`th convergent is
exactly `v`.
-/
theorem of_correctness_of_terminates (terminates : (of v).Terminates) : ∃ n : ℕ, v = (of v).convs n :=
  Exists.elim terminates fun n terminatedAt_n => Exists.intro n (of_correctness_of_terminatedAt terminatedAt_n)

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