Theorems · Theorem · general topology
Filter.Frequently.mp
∀ {α : Type u} {p q : α → Prop} {f : Filter α},
(∃ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, p x → q x) → ∃ᶠ (x : α) in f, q x- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 12 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 by12
Results whose statement or proof uses this declaration.
- Filter.Frequently.monoproof · cited by 64
- Filter.frequently_congrproof · cited by 6
- ContinuousMapZero.induction_on_of_compactproof · cited by 4
- HasDerivWithinAt.liminf_right_slope_norm_leproof · cited by 3
- ContinuousMap.induction_on_of_compactproof · cited by 2
- MeasureTheory.not_tendsto_diracProba_of_not_tendstoproof · cited by 1
- StarConvex.smul_vadd_mem_of_isClosed_of_mem_asymptoticConeproof · cited by 1
- AnalyticOnNhd.eq_zero_or_eq_zero_of_smul_eq_zeroproof · cited by 1
- MeasureTheory.Measure.AbsolutelyContinuous.support_monoproof · cited by 1
- isCountablyCompact_iff_infinite_subset_has_accPtproof · cited by 0
- UpperHemicontinuousAt.mem_of_tendstoproof · cited by 0
- Convex.smul_vadd_mem_of_mem_nhds_of_mem_asymptoticConeproof · cited by 0