exists_rat_eq_of_terminates — Mathlib

English

If GenContFract.of v terminates, there exists q ∈ ℚ with v = ↑q.

Русский

Если GenContFract.of v завершается, то существует q ∈ ℚ такое, что v = ↑q.

LaTeX

$$$\\text{Terminates}(\\mathrm{GenContFract.of}\\, v) \\rightarrow \\exists q : \\mathbb{Q}, v = (q : K)$$$

Lean4

/-- Every terminating continued fraction corresponds to a rational number. -/
theorem exists_rat_eq_of_terminates (terminates : (of v).Terminates) : ∃ q : ℚ, v = ↑q :=
  by
  obtain ⟨n, v_eq_conv⟩ : ∃ n, v = (of v).convs n := of_correctness_of_terminates terminates
  obtain ⟨q, conv_eq_q⟩ : ∃ q : ℚ, (of v).convs n = (↑q : K) := exists_rat_eq_nth_conv v n
  have : v = (↑q : K) := Eq.trans v_eq_conv conv_eq_q
  use q, this

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