Theorems · Theorem · general topology
Filter.Eventually.and_frequently
∀ {α : 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
- 7 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext, 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.Eventuallystatement and proof · cited by 3,134
- Filter.Frequentlystatement and proof · cited by 414
- Filter.Frequently.and_eventuallyproof · cited by 49
Cited by7
Results whose statement or proof uses this declaration.
- LiouvilleWith.exists_posproof · cited by 4
- LiouvilleWith.frequently_lt_rpow_negproof · cited by 3
- Liouville.liouvilleWithproof · cited by 2
- Filter.liminf_le_limsup_of_frequently_leproof · cited by 2
- LiouvilleWith.ne_cast_intproof · cited by 1
- Asymptotics.isLittleO_irrefl'proof · cited by 1
- forall_liouvilleWith_iffproof · cited by 0