Theorems · Theorem · general topology
Filter.Frequently.and_eventually
∀ {α : Type u} {p q : α → Prop} {f : Filter α},
(∃ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, q x) → ∃ᶠ (x : α) in f, p x ∧ q x- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
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.Eventuallystatement and proof · cited by 3,134
- Filter.Eventually.monoproof · cited by 646
- Filter.Frequentlystatement and proof · cited by 414
- Filter.Eventually.mpproof · cited by 78
Cited by49
Results whose statement or proof uses this declaration.
- Filter.le_limsup_of_frequently_leproof · cited by 10
- Filter.Eventually.and_frequentlyproof · cited by 7
- Filter.Eventually.exists_gtproof · cited by 7
- VitaliFamily.measure_le_of_frequently_leproof · cited by 5
- ClusterPt.limsSupproof · 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