Theorems · Theorem · general topology
Filter.Frequently.exists
∀ {α : Type u} {p : α → Prop} {f : Filter α}, (∃ᶠ (x : α) in f, p x) → ∃ x, p x- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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.Eventuallyproof · cited by 3,134
- Filter.Eventually.of_forallproof · cited by 526
- Filter.Frequentlystatement and proof · cited by 414
Cited by32
Results whose statement or proof uses this declaration.
- Filter.Eventually.existsproof · cited by 168
- Filter.le_limsup_of_frequently_leproof · cited by 10
- Filter.Eventually.exists_gtproof · cited by 7
- Filter.liminf_le_of_frequently_le'proof · cited by 4
- image_le_of_liminf_slope_right_lt_deriv_boundary'proof · cited by 4
- BoundedVariationOn.tendsto_eVariationOn_Ici_zero_of_filterproof · cited by 3
- Filter.IsCobounded.of_frequently_geproof · cited by 3
- Filter.IsCobounded.of_frequently_leproof · cited by 3
- MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'proof · cited by 3
- TendstoLocallyUniformlyOn.continuousOnproof · cited by 3
- MeasureTheory.NullMeasurableSet.right_of_prodproof · cited by 3
- Filter.isBoundedUnder_le_mul_of_nonnegproof · cited by 2