Theorems · Theorem · general topology

Filter.Eventually.and

∀ {α : Type u} {p q : α → Prop} {f : Filter α},
  Filter.Eventually p f → Filter.Eventually q f → ∀ᶠ (x : α) in f, p x ∧ q x

Defined in

Mathlib.Order.Filter.Basic

Cited by

157 results in Mathlib

Foundations

Depth 8 from the axioms, rests on 16 definitions · uses no axioms