mathlib3 documentation

order.filter.ultrafilter

Ultrafilters #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
def filter.is_atomic {α : Type u} :

filter α is an atomic type: for every filter there exists an ultrafilter that is less than or equal to this filter.

@[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 α) :
@[protected]
theorem ultrafilter.is_atom {α : 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
theorem ultrafilter.inf_ne_bot_iff {α : Type u} {f : ultrafilter α} {g : filter α} :
theorem ultrafilter.disjoint_iff_not_le {α : Type u} {f : ultrafilter α} {g : filter α} :
@[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 the forward direction of ultrafilter.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
def ultrafilter.of_atom {α : Type u} (f : filter α) (hf : is_atom f) :

If f : filter α is an atom, then it is an ultrafilter.

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 α} :
@[simp]
theorem ultrafilter.le_sup_iff {α : Type u} {u : ultrafilter α} {f g : filter α} :
u f g u f u g
@[simp]
theorem ultrafilter.union_mem_iff {α : Type u} {f : ultrafilter α} {s t : set α} :
s t f s f t f
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.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 x q 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 β} :
@[simp]
theorem ultrafilter.map_id {α : Type u} (f : ultrafilter α) :
@[simp]
theorem ultrafilter.map_id' {α : Type u} (f : ultrafilter α) :
ultrafilter.map (λ (x : α), x) f = f
@[simp]
theorem ultrafilter.map_map {α : Type u} {β : Type v} {γ : Type u_1} (f : ultrafilter α) (m : α β) (n : β γ) :
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, norm_cast]
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
@[simp]
theorem ultrafilter.comap_id {α : Type u} (f : ultrafilter α) (h₀ : function.injective id := function.injective_id) (h₁ : set.range id f := _) :
f.comap h₀ h₁ = f
@[simp]
theorem ultrafilter.comap_comap {α : Type u} {β : Type v} {γ : Type u_1} (f : ultrafilter γ) {m : α β} {n : β γ} (inj₀ : function.injective n) (large₀ : set.range n f) (inj₁ : function.injective m) (large₁ : set.range m f.comap inj₀ large₀) (inj₂ : function.injective (n m) := _) (large₂ : set.range (n m) f := _) :
(f.comap inj₀ large₀).comap inj₁ large₁ = f.comap inj₂ large₂
@[protected, instance]

The principal ultrafilter associated to a point x.

Equations
@[simp]
theorem ultrafilter.mem_pure {α : Type u} {a : α} {s : set α} :
@[simp]
theorem ultrafilter.coe_pure {α : Type u} (a : α) :
@[simp]
theorem ultrafilter.map_pure {α : Type u} {β : Type v} (m : α β) (a : α) :
@[simp]
theorem ultrafilter.comap_pure {α : Type u} {β : Type v} {m : α β} (a : α) (inj : function.injective m) (large : set.range m has_pure.pure (m a)) :
(has_pure.pure (m a)).comap inj large = has_pure.pure a
@[protected, instance]
theorem ultrafilter.eq_pure_of_finite_mem {α : Type u} {f : ultrafilter α} {s : set α} (h : s.finite) (h' : s f) :
(x : α) (H : x s), f = has_pure.pure x
theorem ultrafilter.eq_pure_of_finite {α : Type u} [finite α] (f : ultrafilter α) :
(a : α), f = has_pure.pure a
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
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 ultrafilter.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 filter.is_atom_pure {α : Type u} {a : α} :
@[protected]
theorem filter.ne_bot.le_pure_iff {α : Type u} {f : filter α} {a : α} (hf : f.ne_bot) :
@[simp]
theorem filter.lt_pure_iff {α : Type u} {f : filter α} {a : α} :
theorem filter.le_pure_iff' {α : Type u} {f : filter α} {a : α} :
@[simp]
theorem filter.Iic_pure {α : Type u} (a : α) :
theorem filter.mem_iff_ultrafilter {α : Type u} {f : filter α} {s : set α} :
s f (g : ultrafilter α), g f s 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_bot f g p f) (f : ultrafilter α), f g p f
noncomputable def filter.hyperfilter (α : Type u) [infinite α] :

The ultrafilter extending the cofinite filter.

Equations
theorem filter.nmem_hyperfilter_of_finite {α : 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) :