Ultrafilters

An ultrafilter is a minimal (maximal in the set order) proper filter. In this file we define

is_ultrafilter: a predicate stating that a given filter is an ultrafiler;
ultrafilter_of: an ultrafilter that is less than or equal to a given filter;
ultrafilter: subtype of ultrafilters;
ultrafilter.pure: pure x as an ultrafiler;
ultrafilter.map, ultrafilter.bind : operations on ultrafilters;
hyperfilter: the ultra-filter extending the cofinite filter.

source

def filter.is_ultrafilter {α : Type u} (f : filter α) :

Prop

An ultrafilter is a minimal (maximal in the set order) proper filter.

Equations

f.is_ultrafilter = (f.ne_bot ∧ ∀ (g : filter α), g.ne_bot → g ≤ f → f ≤ g)

source

theorem filter.is_ultrafilter.unique {α : Type u} {f g : filter α} (hg : g.is_ultrafilter) (hf : f.ne_bot) (h : f ≤ g) :

f = g

source

theorem filter.le_of_ultrafilter {α : Type u} {f g : filter α} (hf : f.is_ultrafilter) (h : (g ⊓ f).ne_bot) :

f ≤ g

source

theorem filter.ultrafilter_iff_compl_mem_iff_not_mem {α : Type u} {f : filter α} :

f.is_ultrafilter ↔ ∀ (s : set α), sᶜ ∈ f ↔ s ∉ f

Equivalent characterization of ultrafilters: A filter f is an ultrafilter if and only if for each set s, -s belongs to f if and only if s does not belong to f.

source

theorem filter.mem_or_compl_mem_of_ultrafilter {α : Type u} {f : filter α} (hf : f.is_ultrafilter) (s : set α) :

s ∈ f ∨ sᶜ ∈ f

source

theorem filter.mem_or_mem_of_ultrafilter {α : Type u} {f : filter α} {s t : set α} (hf : f.is_ultrafilter) (h : s ∪ t ∈ f) :

s ∈ f ∨ t ∈ f

source

theorem filter.is_ultrafilter.em {α : Type u} {f : filter α} (hf : f.is_ultrafilter) (p : α → Prop) :

(∀ᶠ (x : α) in f, p x) ∨ ∀ᶠ (x : α) in f, ¬p x

source

theorem filter.is_ultrafilter.eventually_or {α : Type u} {f : filter α} (hf : f.is_ultrafilter) {p q : α → Prop} :

(∀ᶠ (x : α) in f, p x ∨ q x) ↔ (∀ᶠ (x : α) in f, p x) ∨ ∀ᶠ (x : α) in f, q x

source

theorem filter.is_ultrafilter.eventually_not {α : Type u} {f : filter α} (hf : f.is_ultrafilter) {p : α → Prop} :

(∀ᶠ (x : α) in f, ¬p x) ↔ ¬∀ᶠ (x : α) in f, p x

source

theorem filter.is_ultrafilter.eventually_imp {α : Type u} {f : filter α} (hf : f.is_ultrafilter) {p q : α → Prop} :

(∀ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, q x)

source

theorem filter.mem_of_finite_sUnion_ultrafilter {α : Type u} {f : filter α} {s : set (set α)} (hf : f.is_ultrafilter) (hs : s.finite) (a : ⋃₀s ∈ f) :

∃ (t : set α) (H : t ∈ s), t ∈ f

source

theorem filter.mem_of_finite_Union_ultrafilter {α : Type u} {β : Type v} {f : filter α} {is : set β} {s : β → set α} (hf : f.is_ultrafilter) (his : is.finite) (h : (⋃ (i : β) (H : i ∈ is), s i) ∈ f) :

∃ (i : β) (H : i ∈ is), s i ∈ f

source

theorem filter.ultrafilter_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} (h : f.is_ultrafilter) :

(filter.map m f).is_ultrafilter

source

theorem filter.ultrafilter_pure {α : Type u} {a : α} :

(pure a).is_ultrafilter

source

theorem filter.ultrafilter_bind {α : Type u} {β : Type v} {f : filter α} (hf : f.is_ultrafilter) {m : α → filter β} (hm : ∀ (a : α), (m a).is_ultrafilter) :

(f.bind m).is_ultrafilter

source

theorem filter.exists_ultrafilter {α : Type u} (f : filter α) [h : f.ne_bot] :

∃ (u : filter α), u ≤ f ∧ u.is_ultrafilter

The ultrafilter lemma: Any proper filter is contained in an ultrafilter.

source

def filter.ultrafilter_of {α : Type u} (f : filter α) :

filter α

Construct an ultrafilter extending a given filter. The ultrafilter lemma is the assertion that such a filter exists; we use the axiom of choice to pick one.

Equations