Theorems · Theorem · general topology
Filter.Eventually.of_forall
∀ {α : Type u} {p : α → Prop} {f : Filter α}, (∀ (x : α), p x) → ∀ᶠ (x : α) in f, p x- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 526 results in Mathlib
- Foundations
- Depth 9 from the axioms, rests on 17 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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 · cited by 3,134
- Filter.univ_mem'proof · cited by 1,672
Cited by526
Results whose statement or proof uses this declaration.
- Filter.Eventually.monoproof · cited by 646
- MeasureTheory.ae_of_allproof · cited by 137
- Filter.EventuallyEq.reflproof · cited by 108
- Filter.isBounded_le_of_topproof · cited by 75
- Filter.Frequently.monoproof · cited by 64
- Filter.isBounded_ge_of_botproof · cited by 55
- tendsto_of_tendsto_of_tendsto_of_le_of_leproof · cited by 35
- MeasureTheory.setIntegral_congr_funproof · cited by 35
- Filter.Frequently.existsproof · cited by 32
- MeasureTheory.setLIntegral_congr_funproof · cited by 31
- NormedSpace.expSeries_radius_eq_topproof · cited by 27
- Filter.Frequently.of_forallproof · cited by 25
Showing the 200 most cited of 526.