evaln_bound — Mathlib

English

If x ∈ evaln k c n, then n < k.

Русский

Если x принадлежит evaln k c n, то n < k.

LaTeX

$$$\\forall k\\,c\\,n\\,x,\\ x \\in \\mathrm{evaln}(k,c,n) \\Rightarrow n < k$$$

Lean4

theorem evaln_bound : ∀ {k c n x}, x ∈ evaln k c n → n < k
  | 0, c, n, x, h => by simp [evaln] at h
  | k + 1, c, n, x, h =>
    by
    suffices
      ∀ {o : Option ℕ},
        x ∈ do {
            guard (n ≤ k);
            o
            } →
          n < k + 1
      by cases c <;> rw [evaln] at h <;> exact this h
    simpa [Option.bind_eq_some_iff] using Nat.lt_succ_of_le

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