lean_workbook_plus_20802
Proved- and :
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20802 (f : ℕ → ℕ) (hf: f 1 = 1 ∧ ∀ n ≥ 2, n ≥ f n ∧ f n ≥ 2) : ∃ n, n ≥ f n ∧ f n ≥ 2 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_20802 (f : ℕ → ℕ) (hf: f 1 = 1 ∧ ∀ n ≥ 2, n ≥ f n ∧ f n ≥ 2) : ∃ n, n ≥ f n ∧ f n ≥ 2 := by sorry