of_s_head_aux — Mathlib

English

The head of the continued fraction for non-integer v can be expressed as the pair with a = 1 and b = floor of the inverse of fract(v).

Русский

Головной член непрерывной дроби для нецелого v задан как пара (1, floor(fract(v)^{-1})).

LaTeX

$$$\text{If } \operatorname{fract}(v) \neq 0,\; (\operatorname{of} v).s.head = \mathrm{Some}(\langle 1, \lfloor(\operatorname{fract} v)^{-1}\rfloor\rangle)$$$

Lean4

theorem of_s_head_aux (v : K) :
    (of v).s.get? 0 =
      (IntFractPair.stream v 1).bind
        (some ∘ fun p =>
          { a := 1
            b := p.b }) :=
  by
  rw [of, IntFractPair.seq1]
  simp only [Stream'.Seq.map, Stream'.Seq.tail, Stream'.Seq.get?, Stream'.map]
  rw [← Stream'.get_succ, Stream'.get, Option.map.eq_def]
  split <;> simp_all only [Option.bind_some, Option.bind_none, Function.comp_apply]

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