Theorems · Theorem · general topology

Filter.frequently_congr

∀ {α : Type u} {p q : α → Prop} {f : Filter α},
  (∀ᶠ (x : α) in f, p x ↔ q x) → ((∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x)

Defined in

Mathlib.Order.Filter.Basic

Cited by

6 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms