succ_nth_fib_le_of_nth_den — Mathlib

English

There exists a z ∈ Z such that b = z for any partDen b coming from the construction of GenContFract.of v.

Русский

Существуют целые z такие, что каждая частьDen b равна z.

LaTeX

$$$\\\\forall {K} {v} {n} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] {b : K},\n (GenContFract.of v).partDens.get? n = Some b \\\\Rightarrow \\\\exists z : \\\\mathbb{Z}, b = (z : K)$$$

Lean4

/-- Shows that the `n`th denominator is greater than or equal to the `n + 1`th fibonacci number,
that is `Nat.fib (n + 1) ≤ Bₙ`. -/
theorem succ_nth_fib_le_of_nth_den (hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)) : (fib (n + 1) : K) ≤ (of v).dens n :=
  by
  rw [den_eq_conts_b, nth_cont_eq_succ_nth_contAux]
  have : n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1) := by
    cases n with
    | zero => exact Or.inl <| le_refl 1
    | succ n => exact Or.inr (Or.resolve_left hyp n.succ_ne_zero)
  exact fib_le_of_contsAux_b this

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