Infinite occurrences

def Cslib.ωSequence.infOcc {α : Type u} (xs : ωSequence α) : Set α

The set of elements that appear infinitely often in an ω-sequence.

Equations

• xs.infOcc = {x : α | ∃ᶠ (k : ℕ) in Filter.atTop, xs k = x}

theorem Cslib.ωSequence.frequently_iff_strictMono {p : ℕ → Prop} : (∃ᶠ (n : ℕ) in Filter.atTop, p n) ↔ ∃ (f : ℕ → ℕ), StrictMono f ∧ ∀ (m : ℕ), p (f m)

An alternative characterization of "infinitely often".