Theorems · Theorem · general topology

Filter.eventually_congr

∀ {α : Type u} {f : Filter α} {p q : α → Prop},
  (∀ᶠ (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

20 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext, Quot.sound