of_correctness_of_terminatedAt — Mathlib

English

If GenContFract.of v terminates at step n, then the value v equals the nth convergent: v = (of v).convs n.

Русский

Если GenContFract.of v прерывается на шаге n, то величина v равна n-му конвергенту: v = (of v).convs n.

LaTeX

$$$(\\mathrm{TerminatedAt}\\ v\\ n) \\rightarrow v = (\\mathrm{of}\\, v).convs n$$$

Lean4

/-- If `GenContFract.of v` terminated at step `n`, then the `n`th convergent is exactly `v`. -/
theorem of_correctness_of_terminatedAt (terminatedAt_n : (of v).TerminatedAt n) : v = (of v).convs n :=
  have : IntFractPair.stream v (n + 1) = none :=
    of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none.1 terminatedAt_n
  of_correctness_of_nth_stream_eq_none this

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