Theorems · Theorem · general topology

Filter.eventually_iff_seq_eventually

∀ {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated],
  (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Filter.Tendsto x Filter.atTop l → ∀ᶠ (n : ℕ) in Filter.atTop, p (x n)

Defined in

Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Cited by

1 results in Mathlib

Foundations

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

Assumes

Filter.IsCountablyGenerated