of_s_of_int — Mathlib

English

The tail of the s-sequence of v is the s-sequence of the inverse fractional part: (of v).s.tail = (of (fract v)^{-1}).s.

Русский

Хвост последовательности s числа v равен последовательности s от обратной дробной части: (of v).s.tail = (of (fract v)^{-1}).s.

LaTeX

$$$\,(\text{of } v).s.tail = (\text{of } (\operatorname{fract} v)^{-1}).s$$$

Lean4

/-- If `a` is an integer, then the coefficient sequence of its continued fraction is empty.
-/
theorem of_s_of_int (a : ℤ) : (of (a : K)).s = Stream'.Seq.nil :=
  haveI h : ∀ n, (of (a : K)).s.get? n = none := by
    intro n
    induction n with
    | zero => rw [of_s_head_aux, stream_succ_of_int, Option.bind]
    | succ n ih => exact (of (a : K)).s.prop ih
  Stream'.Seq.ext fun n => (h n).trans (Stream'.Seq.get?_nil n).symm

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