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".

theorem Cslib.ωSequence.frequently_in_finite_type {α : Type u} [Finite α] {s : Set α} {xs : ωSequence α} : (∃ᶠ (k : ℕ) in Filter.atTop, xs k ∈ s) ↔ ∃ x ∈ s, ∃ᶠ (k : ℕ) in Filter.atTop, xs k = x

In a finite type, the elements of a set occurs infinitely often iff some element in the set occurs infinitely often.