noncomputable def ENat.find (P : ℕ → Prop) : ℕ∞

Equations

• ENat.find P = if h : ∃ (x : ℕ), P x then ↑(Nat.find h) else ⊤

theorem ENat.lt_find (P : ℕ → Prop) (n : ℕ) (h : ∀ m ≤ n, ¬P m) : ↑n < find P

theorem ENat.exists_of_find_le (P : ℕ → Prop) (n : ℕ) (h : find P ≤ ↑n) : ∃ m ≤ n, P m

theorem ENat.find_eq_top_iff (P : ℕ → Prop) : find P = ⊤ ↔ ∀ (n : ℕ), ¬P n

theorem ENat.find_le (P : ℕ → Prop) (n : ℕ) (h : P n) : find P ≤ ↑n