def eventually (p : ℕ → Prop) : Prop

Equations

• eventually p = ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → p n

theorem eventually_and {p q : ℕ → Prop} : (eventually fun (n : ℕ) => p n ∧ q n) ↔ eventually p ∧ eventually q

@[simp]

theorem not_eventually_even : ¬eventually Even

@[simp]

theorem not_eventually_odd : ¬eventually Odd

theorem eventually_or_of {p q : ℕ → Prop} (h : eventually p ∨ eventually q) : eventually fun (n : ℕ) => p n ∨ q n

@[simp]

theorem eventually_const {P : Prop} : (eventually fun (x : ℕ) => P) ↔ P

theorem exi_of_eventually {p : ℕ → Prop} (h : eventually p) : ∃ (n : ℕ), p n

theorem eventually_iff_exi_least {p : ℕ → Prop} : eventually p ↔ (∀ (n : ℕ), p n) ∨ ∃ (N : ℕ), ¬p N ∧ ∀ (n : ℕ), N < n → p n