Theorems · Theorem · general topology

Filter.coext

∀ {α : Type u} {f g : Filter α}, (∀ (s : Set α), sᶜ ∈ f ↔ sᶜ ∈ g) → f = g

An extensionality lemma that is useful for filters with good lemmas about sᶜ ∈ f (e.g., Filter.comap, Filter.coprod, Filter.Coprod, Filter.cofinite).

Defined in

Mathlib.Order.Filter.Basic

Cited by

3 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound