Theorems · Theorem · general topology
Filter.Frequently.of_forall
∀ {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop}, (∀ (x : α), p x) → ∃ᶠ (x : α) in f, p x- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Filter.NeBot
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.NeBotstatement and proof · cited by 853
- Filter.Eventually.of_forallproof · cited by 526
- Filter.Frequentlystatement · cited by 414
- Filter.Eventually.frequentlyproof · cited by 44
Cited by25
Results whose statement or proof uses this declaration.
- Antitone.map_limsSup_of_continuousAtproof · cited by 6
- ProbabilityTheory.Kernel.density_nonnegproof · cited by 5
- continuousOn_tsumproof · cited by 3
- Filter.IsCobounded.frequently_geproof · cited by 3
- Filter.IsCobounded.frequently_leproof · cited by 3
- tendsto_subseq_of_boundedproof · cited by 3
- HasFPowerSeriesWithinOnBall.continuousOnproof · cited by 2
- MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_leproof · cited by 2
- MeasurableSet.iUnion_of_monotoneproof · cited by 2
- ENNReal.ofReal_limsup_toRealproof · cited by 1
- IsSeqCompact.exists_tendstoproof · cited by 1
- NNReal.toReal_limsupproof · cited by 1