Theorems · Theorem · general topology
Filter.frequently_iff_seq_forall
∀ {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated],
(∃ᶠ (n : ι) in l, p n) ↔ ∃ ns, Filter.Tendsto ns Filter.atTop l ∧ ∀ (n : ℕ), p (ns n)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 76 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.
Cites8
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.atTopstatement and proof · cited by 2,405
- Filter.Frequentlystatement and proof · cited by 414
- Filter.IsCountablyGeneratedstatement and proof · cited by 220
- Filter.Frequently.of_forallproof · cited by 25
- Filter.Tendsto.frequentlyproof · cited by 12
- Filter.exists_seq_forall_of_frequentlyproof · cited by 7
Cited by1
Results whose statement or proof uses this declaration.
- ProbabilityTheory.eqOn_complexMGF_of_mgf'proof · cited by 1