Theorems · Theorem · general topology
Filter.exists_seq_forall_of_frequently
∀ {ι : 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
- 7 results in Mathlib
- Foundations
- Depth 75 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.atTopstatement and proof · cited by 2,405
- Filter.Frequentlystatement and proof · cited by 414
- Filter.IsCountablyGeneratedstatement and proof · cited by 220
- Filter.subseq_forall_of_frequentlyproof · cited by 1
- Filter.frequently_iff_seq_frequentlyproof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- IsLUB.exists_seq_strictMono_tendsto_of_notMemproof · cited by 4
- Filter.tendsto_of_subseq_tendstoproof · cited by 3
- MeasurableSet.iUnion_of_monotone_of_frequentlyproof · cited by 2
- Filter.frequently_iff_seq_forallproof · cited by 1
- MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous'proof · cited by 1
- UpperHemicontinuousAt.of_sequencesproof · cited by 1
- LowerHemicontinuousAt.of_sequencesproof · cited by 0