le_fib_self — Mathlib

English

The function fib is monotone on natural numbers with respect to ≤.

Русский

Функция fib монотонна по отношению к неубыванию на натуральных числах.

LaTeX

$$fib is monotone with respect to ≤$$

Lean4

theorem le_fib_self {n : ℕ} (five_le_n : 5 ≤ n) : n ≤ fib n := by
  induction five_le_n with
  | refl =>
    rfl -- 5 ≤ fib 5

  | @step n five_le_n IH => -- n + 1 ≤ fib (n + 1) for 5 ≤ n

    rw [succ_le_iff]
    calc
      n ≤ fib n := IH
      _ < fib (n + 1) := fib_lt_fib_succ (le_trans (by decide) five_le_n)

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