mathlib documentation

order.filter.ultrafilter

Ultrafilters #

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

structure ultrafilter (α : Type u_1) :
Type u_1

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

@[protected, instance]
def ultrafilter.filter.has_coe_t {α : Type u} :
Equations
@[protected, instance]
def ultrafilter.has_mem {α : Type u} :
Equations
theorem ultrafilter.unique {α : Type u} (f : ultrafilter α) {g : filter α} (h : g f) (hne : g.ne_bot . "apply_instance") :
g = f
@[protected, instance]
def ultrafilter.ne_bot {α : Type u} (f : ultrafilter α) :
@[simp, norm_cast]
theorem ultrafilter.mem_coe {α : Type u} {f : ultrafilter α} {s : set α} :
s f s f
theorem ultrafilter.eq_of_le {α : Type u} {f g : ultrafilter α} (h : f g) :
f = g
@[simp, norm_cast]
theorem ultrafilter.coe_le_coe {α : Type u} {f g : ultrafilter α} :
f g f = g
@[simp, norm_cast]
theorem ultrafilter.coe_inj {α : Type u} {f g : ultrafilter α} :
f = g f = g
@[ext]
theorem ultrafilter.ext {α : Type u} ⦃f g : ultrafilter α⦄ (h : ∀ (s : set α), s f s g) :
f = g
theorem ultrafilter.le_of_inf_ne_bot {α : Type u} (f : ultrafilter α) {g : filter α} (hg : (f g).ne_bot) :
f g
theorem ultrafilter.le_of_inf_ne_bot' {α : Type u} (f : ultrafilter α) {g : filter α} (hg : (g f).ne_bot) :
f g
@[simp]
theorem ultrafilter.compl_not_mem_iff {α : Type u} {f : ultrafilter α} {s : set α} :
s f s f
@[simp]
theorem ultrafilter.frequently_iff_eventually {α : Type u} {f : ultrafilter α} {p : α → Prop} :
(∃ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, p x
theorem filter.frequently.eventually {α : Type u} {f : ultrafilter α} {p : α → Prop} :
(∃ᶠ (x : α) in f, p x)(∀ᶠ (x : α) in f, p x)

Alias of frequently_iff_eventually.

theorem ultrafilter.compl_mem_iff_not_mem {α : Type u} {f : ultrafilter α} {s : set α} :
s f s f
theorem ultrafilter.diff_mem_iff {α : Type u} {s t : set α} (f : ultrafilter α) :
s \ t f s f t f
def ultrafilter.of_compl_not_mem_iff {α : Type u} (f : filter α) (h : ∀ (s : set α), s f s f) :

If sᶜ ∉ f ↔ s ∈ f, then f is an ultrafilter. The other implication is given by ultrafilter.compl_not_mem_iff.

Equations
theorem ultrafilter.nonempty_of_mem {α : Type u} {f : ultrafilter α} {s : set α} (hs : s f) :
theorem ultrafilter.ne_empty_of_mem {α : Type u} {f : ultrafilter α} {s : set α} (hs : s f) :
@[simp]
theorem ultrafilter.empty_not_mem {α : Type u} {f : ultrafilter α} :
theorem ultrafilter.mem_or_compl_mem {α : Type u} (f : ultrafilter α) (s : set α) :
s f s f
@[protected]
theorem ultrafilter.em {α : Type u} (f : ultrafilter α) (p : α → Prop) :
(∀ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, ¬p x
theorem ultrafilter.eventually_or {α : Type u} {f : ultrafilter α} {p q : α → Prop} :
(∀ᶠ (x : α) in f, p x q x) (∀ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, q x
theorem ultrafilter.union_mem_iff {α : Type u} {f : ultrafilter α} {s t : set α} :
s t f s f t f
theorem ultrafilter.eventually_not {α : Type u} {f : ultrafilter α} {p : α → Prop} :
(∀ᶠ (x : α) in f, ¬p x) ¬∀ᶠ (x : α) in f, p x
theorem ultrafilter.eventually_imp {α : Type u} {f : ultrafilter α} {p q : α → Prop} :
(∀ᶠ (x : α) in f, p xq x) (∀ᶠ (x : α) in f, p x)(∀ᶠ (x : α) in f, q x)
theorem ultrafilter.finite_sUnion_mem_iff {α : Type u} {f : ultrafilter α} {s : set (set α)} (hs : s.finite) :
⋃₀s f ∃ (t : set α) (H : t s), t f
theorem ultrafilter.finite_bUnion_mem_iff {α : Type u} {β : Type v} {f : ultrafilter α} {is : set β} {s : β → set α} (his : is.finite) :
(⋃ (i : β) (H : i is), s i) f ∃ (i : β) (H : i is), s i f
def ultrafilter.map {α : Type u} {β : Type v} (m : α → β) (f : ultrafilter α) :

Pushforward for ultrafilters.

Equations
@[simp, norm_cast]
theorem ultrafilter.coe_map {α : Type u} {β : Type v} (m : α → β) (f : ultrafilter α) :
@[simp]
theorem ultrafilter.mem_map {α : Type u} {β : Type v} {m : α → β} {f : ultrafilter α} {s : set β} :
def ultrafilter.comap {α : Type u} {β : Type v} {m : α → β} (u : ultrafilter β) (inj : function.injective m) (large : set.range m u) :

The pullback of an ultrafilter along an injection whose range is large with respect to the given ultrafilter.

Equations
@[simp]
theorem ultrafilter.mem_comap {α : Type u} {β : Type v} {m : α → β} (u : ultrafilter β) (inj : function.injective m) (large : set.range m u) {s : set α} :
s u.comap inj large m '' s u
@[simp]
theorem ultrafilter.coe_comap {α : Type u} {β : Type v} {m : α → β} (u : ultrafilter β) (inj : function.injective m) (large : set.range m u) :
(u.comap inj large) = filter.comap m u
@[protected, instance]

The principal ultrafilter associated to a point x.

Equations
@[simp]
theorem ultrafilter.mem_pure {α : Type u} {a : α} {s : set α} :
s pure a a s
@[protected, instance]
def ultrafilter.inhabited {α : Type u} [inhabited α] :
Equations
@[protected, instance]
def ultrafilter.nonempty {α : Type u} [nonempty α] :
theorem ultrafilter.eq_principal_of_finite_mem {α : Type u} {f : ultrafilter α} {s : set α} (h : s.finite) (h' : s f) :
∃ (x : α) (H : x s), f = pure x
def ultrafilter.bind {α : Type u} {β : Type v} (f : ultrafilter α) (m : α → ultrafilter β) :

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

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem ultrafilter.exists_le {α : Type u} (f : filter α) [h : f.ne_bot] :
∃ (u : ultrafilter α), u f

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

theorem filter.exists_ultrafilter_le {α : Type u} (f : filter α) [h : f.ne_bot] :
∃ (u : ultrafilter α), u f

Alias of exists_le.

noncomputable def ultrafilter.of {α : Type u} (f : filter α) [f.ne_bot] :

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 ultrafilter.of_le {α : Type u} (f : filter α) [f.ne_bot] :
theorem ultrafilter.of_coe {α : Type u} (f : ultrafilter α) :
theorem ultrafilter.exists_ultrafilter_of_finite_inter_nonempty {α : Type u} (S : set (set α)) (cond : ∀ (T : finset (set α)), T S(⋂₀ T).nonempty) :
∃ (F : ultrafilter α), S F.to_filter.sets
theorem filter.mem_iff_ultrafilter {α : Type u} {s : set α} {f : filter α} :
s f ∀ (g : ultrafilter α), g fs g
theorem filter.le_iff_ultrafilter {α : Type u} {f₁ f₂ : filter α} :
f₁ f₂ ∀ (g : ultrafilter α), g f₁g f₂
theorem filter.supr_ultrafilter_le_eq {α : Type u} (f : filter α) :
(⨆ (g : ultrafilter α) (hg : g f), g) = f

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

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

The tendsto relation can be checked on ultrafilters.

theorem filter.exists_ultrafilter_iff {α : Type u} {f : filter α} :
(∃ (u : ultrafilter α), u f) f.ne_bot
theorem filter.forall_ne_bot_le_iff {α : Type u} {g : filter α} {p : filter α → Prop} (hp : monotone p) :
(∀ (f : filter α), f.ne_botf gp f) ∀ (f : ultrafilter α), f gp f
noncomputable def filter.hyperfilter (α : Type u) [infinite α] :

The ultrafilter extending the cofinite filter.

Equations
@[simp]
theorem filter.bot_ne_hyperfilter {α : Type u} [infinite α] :
theorem filter.nmem_hyperfilter_of_finite {α : Type u} [infinite α] {s : set α} (hf : s.finite) :
theorem set.finite.nmem_hyperfilter {α : Type u} [infinite α] {s : set α} (hf : s.finite) :

Alias of nmem_hyperfilter_of_finite.

theorem filter.compl_mem_hyperfilter_of_finite {α : Type u} [infinite α] {s : set α} (hf : s.finite) :
theorem set.finite.compl_mem_hyperfilter {α : Type u} [infinite α] {s : set α} (hf : s.finite) :

Alias of compl_mem_hyperfilter_of_finite.

theorem filter.mem_hyperfilter_of_finite_compl {α : Type u} [infinite α] {s : set α} (hf : s.finite) :
theorem ultrafilter.comap_inf_principal_ne_bot_of_image_mem {α : Type u} {β : Type v} {m : α → β} {s : set α} {g : ultrafilter β} (h : m '' s g) :
noncomputable def ultrafilter.of_comap_inf_principal {α : Type u} {β : Type v} {m : α → β} {s : set α} {g : ultrafilter β} (h : m '' s g) :

Ultrafilter extending the inf of a comapped ultrafilter and a principal ultrafilter.

Equations
theorem ultrafilter.of_comap_inf_principal_mem {α : Type u} {β : Type v} {m : α → β} {s : set α} {g : ultrafilter β} (h : m '' s g) :
theorem ultrafilter.of_comap_inf_principal_eq_of_map {α : Type u} {β : Type v} {m : α → β} {s : set α} {g : ultrafilter β} (h : m '' s g) :