Theorems · Theorem · general topology

Filter.subseq_forall_of_frequently

∀ {ι : Type u_6} {x : ℕ → ι} {p : ι → Prop} {l : Filter ι},
  Filter.Tendsto x Filter.atTop l →
    (∃ᶠ (n : ℕ) in Filter.atTop, p (x n)) →
      ∃ ns, Filter.Tendsto (fun n => x (ns n)) Filter.atTop l ∧ ∀ (n : ℕ), p (x (ns n))

Defined in

Mathlib.Order.Filter.AtTopBot.Basic

Cited by

1 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound