# mathlibdocumentation

order.filter.ultrafilter

# 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.
def filter.is_ultrafilter {α : Type u} :
→ Prop

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

Equations
theorem filter.is_ultrafilter.unique {α : Type u} {f g : filter α} :
g.is_ultrafilterf.ne_botf gf = g

theorem filter.le_of_ultrafilter {α : Type u} {f g : filter α} :
f.is_ultrafilter(g f).ne_botf g

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.

theorem filter.ultrafilter_iff_compl_mem_iff_not_mem' {α : Type u} {f : filter α} :
f.is_ultrafilter ∀ (s : set α), s f s f

A variant of ultrafilter_iff_compl_mem_iff_not_mem.

theorem filter.nonempty_of_mem_ultrafilter {α : Type u} {f : filter α} {s : set α} :
f.is_ultrafilters f → s.nonempty

theorem filter.ne_empty_of_mem_ultrafilter {α : Type u} {f : filter α} {s : set α} :
f.is_ultrafilters fs

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

theorem filter.mem_or_mem_of_ultrafilter {α : Type u} {f : filter α} {s t : set α} :
f.is_ultrafilters t fs f t f

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

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

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

theorem filter.is_ultrafilter.eventually_imp {α : Type u} {f : filter α} (hf : f.is_ultrafilter) {p q : α → Prop} :
(∀ᶠ (x : α) in f, p xq x) (∀ᶠ (x : α) in f, p x)(∀ᶠ (x : α) in f, q x)

theorem filter.mem_of_finite_sUnion_ultrafilter {α : Type u} {f : filter α} {s : set (set α)} :
f.is_ultrafilters.finite⋃₀s f(∃ (t : set α) (H : t s), t f)

theorem filter.mem_of_finite_Union_ultrafilter {α : Type u} {β : Type v} {f : filter α} {is : set β} {s : β → set α} :
f.is_ultrafilteris.finite(⋃ (i : β) (H : i is), s i) f(∃ (i : β) (H : i is), s i f)

theorem filter.ultrafilter_map {α : Type u} {β : Type v} {f : filter α} {m : α → β} :

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

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

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.

theorem filter.exists_ultrafilter_of_finite_inter_nonempty {α : Type u} (S : set (set α)) :
(∀ (T : finset (set α)), T S → (⋂₀T).nonempty)(∃ (F : filter α), S F.sets F.is_ultrafilter)

def filter.ultrafilter_of {α : Type u} :

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
theorem filter.ultrafilter_of_spec {α : Type u} {f : filter α} [h : f.ne_bot] :

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

theorem filter.ultrafilter_ultrafilter_of {α : Type u} {f : filter α} [f.ne_bot] :

theorem filter.ultrafilter_ultrafilter_of' {α : Type u} {f : filter α} :

@[instance]
def filter.ultrafilter_of_ne_bot {α : Type u} {f : filter α} [h : f.ne_bot] :

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

theorem filter.sup_of_ultrafilters {α : Type u} (f : filter α) :
f = ⨆ (g : filter α) (u : g.is_ultrafilter) (H : g f), g

A filter equals the intersection of all the ultrafilters which contain it.

theorem filter.le_iff_ultrafilter {α : Type u} {l₁ l₂ : filter α} :
l₁ l₂ ∀ (g : filter α), g.is_ultrafilterg l₁g l₂

theorem filter.mem_iff_ultrafilter {α : Type u} {l : filter α} {s : set α} :
s l ∀ (g : filter α), g.is_ultrafilterg ls g

theorem filter.tendsto_iff_ultrafilter {α : Type u} {β : Type v} (f : α → β) (l₁ : filter α) (l₂ : filter β) :
l₁ l₂ ∀ (g : filter α), g.is_ultrafilterg l₁ g l₂

The tendsto relation can be checked on ultrafilters.

def filter.ultrafilter  :
Type uType u

The ultrafilter monad. The monad structure on ultrafilters is the restriction of the one on filters.

Equations
def filter.ultrafilter.map {α : Type u} {β : Type v} :
(α → β)

Push-forward for ultra-filters.

Equations
def filter.ultrafilter.pure {α : Type u} :
α →

The principal ultra-filter associated to a point x.

Equations
def filter.ultrafilter.bind {α : Type u} {β : Type v} :
(α →

Monadic bind for ultra-filters, coming from the one on filters defined in terms of map and join.

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]
def filter.ultrafilter.inhabited {α : Type u} [inhabited α] :

Equations
@[instance]
def filter.filter.ne_bot {α : Type u} {F : filter.ultrafilter α} :

def filter.hyperfilter {α : Type u} :

The ultra-filter extending the cofinite filter.

Equations
theorem filter.hyperfilter_le_cofinite {α : Type u} :

theorem filter.is_ultrafilter_hyperfilter {α : Type u} [infinite α] :

@[instance]
theorem filter.hyperfilter_ne_bot {α : Type u} [infinite α] :

@[simp]
theorem filter.bot_ne_hyperfilter {α : Type u} [infinite α] :

theorem filter.nmem_hyperfilter_of_finite {α : Type u} [infinite α] {s : set α} :

theorem filter.compl_mem_hyperfilter_of_finite {α : Type u} [infinite α] {s : set α} :

theorem filter.mem_hyperfilter_of_finite_compl {α : Type u} [infinite α] {s : set α} :

@[instance]

theorem filter.ultrafilter.eq_iff_val_le_val {α : Type u} {u v : filter.ultrafilter α} :
u = v u.val v.val

theorem filter.exists_ultrafilter_iff {α : Type u} (f : filter α) :
(∃ (u : , u.val f) f.ne_bot