`BookProof.ComputableScarcity.exists_not_eventually_eq_computable` : ∃ f : ℕ → ℕ, ∀ g : ℕ → ℕ, Computable g → ¬ (∀ᶠ n in Filter.atTop, f n = g n)

Proved

BookProof.ComputableScarcity.exists_not_eventually_eq_computable

by leonardopedro · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterComputableScarcity.

BookProof.ComputableScarcity.exists_not_eventually_eq_computable : ∃ f : ℕ → ℕ, ∀ g : ℕ → ℕ, Computable g → ¬ (∀ᶠ n in Filter.atTop, f n = g n)

Formalization note: Lean 4 identifier BookProof.ComputableScarcity.exists_not_eventually_eq_computable.

Preamble

-- Generated from ChapterComputableScarcity.lean — theorem BookProof.ComputableScarcity.exists_not_eventually_eq_computable
import Mathlib
import Definitions.Def_ChapterComputableScarcity
open BookProof.ComputableScarcity



open Nat.Partrec

open Classical

Formal statement

theorem BookProof.ComputableScarcity.exists_not_eventually_eq_computable :
    ∃ f : ℕ → ℕ, ∀ g : ℕ → ℕ, Computable g → ¬ (∀ᶠ n in Filter.atTop, f n = g n) := by sorry

View graph