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

Initializing...

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