Theorems · Theorem · general topology
Filter.frequently_iff_seq_frequently
∀ {ι : 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)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Filter.IsCountablyGenerated
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement and proof · cited by 8,121
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.Eventuallyproof · cited by 3,134
- Filter.atTopstatement and proof · cited by 2,405
- Filter.Frequentlystatement and proof · cited by 414
- Filter.IsCountablyGeneratedstatement and proof · cited by 220
- Filter.eventually_iff_seq_eventuallyproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Filter.exists_seq_forall_of_frequentlyproof · cited by 7