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

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

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

source
structure ultrafilter (α : Type u_2) :
Type u_2

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

Instances for ultrafilter
source
@[protected, instance]
def ultrafilter.filter.has_coe_t {α : Type u} :
has_coe_t (ultrafilter α) (filter α)
Equations
source
@[protected, instance]
def ultrafilter.has_mem {α : Type u} :
has_mem (set α) (ultrafilter α)
Equations
source
theorem ultrafilter.unique {α : Type u} (f : ultrafilter α) {g : filter α} (h : g ≤ ↑f) (hne : g.ne_bot . "apply_instance") :
g = ↑f
source
@[protected, instance]
def ultrafilter.ne_bot {α : Type u} (f : ultrafilter α) :
↑f.ne_bot
source
@[protected]
theorem ultrafilter.is_atom {α : Type u} (f : ultrafilter α) :
is_atom ↑f
source
@[simp, norm_cast]
theorem ultrafilter.mem_coe {α : Type u} {f : ultrafilter α} {s : set α} :
s ∈ ↑f ↔ s ∈ f
source
theorem ultrafilter.coe_injective {α : Type u} :
function.injective coe
source
theorem ultrafilter.eq_of_le {α : Type u} {f g : ultrafilter α} (h : ↑f ≤ ↑g) :
f = g
source
@[simp, norm_cast]
theorem ultrafilter.coe_le_coe {α : Type u} {f g : ultrafilter α} :
↑f ≤ ↑g ↔ f = g
source
@[simp, norm_cast]
theorem ultrafilter.coe_inj {α : Type u} {f g : ultrafilter α} :
↑f = ↑g ↔ f = g
source
@[ext]
theorem ultrafilter.ext {α : Type u} ⦃f g : ultrafilter α⦄ (h : ∀ (s : set α), s ∈ f ↔ s ∈ g) :
f = g
source
theorem ultrafilter.le_of_inf_ne_bot {α : Type u} (f : ultrafilter α) {g : filter α} (hg : (↑f ⊓ g).ne_bot) :
↑f ≤ g
source
theorem ultrafilter.le_of_inf_ne_bot' {α : Type u} (f : ultrafilter α) {g : filter α} (hg : (g ⊓ ↑f).ne_bot) :
↑f ≤ g
source
theorem ultrafilter.inf_ne_bot_iff {α : Type u} {f : ultrafilter α} {g : filter α} :
(↑f ⊓ g).ne_bot ↔ ↑f ≤ g
source
theorem ultrafilter.disjoint_iff_not_le {α : Type u} {f : ultrafilter α} {g : filter α} :
disjoint ↑f g ↔ ¬↑f ≤ g
source
@[simp]
theorem ultrafilter.compl_not_mem_iff {α : Type u} {f : ultrafilter α} {s : set α} :
sᶜ ∉ f ↔ s ∈ f
source
@[simp]
theorem ultrafilter.frequently_iff_eventually {α : Type u} {f : ultrafilter α} {p : α → Prop} :
(∃ᶠ (x : α) in ↑f, p x) ↔ ∀ᶠ (x : α) in ↑f, p x
source
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.

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

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

Equations
source
def ultrafilter.of_atom {α : Type u} (f : filter α) (hf : is_atom f) :
ultrafilter α

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

Equations
source
theorem ultrafilter.nonempty_of_mem {α : Type u} {f : ultrafilter α} {s : set α} (hs : s ∈ f) :
s.nonempty
source
theorem ultrafilter.ne_empty_of_mem {α : Type u} {f : ultrafilter α} {s : set α} (hs : s ∈ f) :
s ≠ ∅
source
@[simp]
theorem ultrafilter.empty_not_mem {α : Type u} {f : ultrafilter α} :
∅ ∉ f
source
@[simp]
theorem ultrafilter.le_sup_iff {α : Type u} {u : ultrafilter α} {f g : filter α} :
↑u ≤ f ⊔ g ↔ ↑u ≤ f ∨ ↑u ≤ g
source
@[simp]
theorem ultrafilter.union_mem_iff {α : Type u} {f : ultrafilter α} {s t : set α} :
s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f
source
theorem ultrafilter.mem_or_compl_mem {α : Type u} (f : ultrafilter α) (s : set α) :
s ∈ f ∨ sᶜ ∈ f
source
@[protected]
theorem ultrafilter.em {α : Type u} (f : ultrafilter α) (p : α → Prop) :
(∀ᶠ (x : α) in ↑f, p x) ∨ ∀ᶠ (x : α) in ↑f, ¬p x
source
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
source
theorem ultrafilter.eventually_not {α : Type u} {f : ultrafilter α} {p : α → Prop} :
(∀ᶠ (x : α) in ↑f, ¬p x) ↔ ¬∀ᶠ (x : α) in ↑f, p x
source
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)
source
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
source
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
source
def ultrafilter.map {α : Type u} {β : Type v} (m : α → β) (f : ultrafilter α) :
ultrafilter β

Pushforward for ultrafilters.

Equations
source
@[simp, norm_cast]
theorem ultrafilter.coe_map {α : Type u} {β : Type v} (m : α → β) (f : ultrafilter α) :
↑(ultrafilter.map m f) = filter.map m ↑f
source
@[simp]
theorem ultrafilter.mem_map {α : Type u} {β : Type v} {m : α → β} {f : ultrafilter α} {s : set β} :
s ∈ ultrafilter.map m f ↔ m ⁻¹' s ∈ f
source
@[simp]
theorem ultrafilter.map_id {α : Type u} (f : ultrafilter α) :
ultrafilter.map id f = f
source
@[simp]
theorem ultrafilter.map_id' {α : Type u} (f : ultrafilter α) :
ultrafilter.map (λ (x : α), x) f = f
source
@[simp]
theorem ultrafilter.map_map {α : Type u} {β : Type v} {γ : Type u_1} (f : ultrafilter α) (m : α → β) (n : β → γ) :
ultrafilter.map n (ultrafilter.map m f) = ultrafilter.map (n ∘ m) f
source
def ultrafilter.comap {α : Type u} {β : Type v} {m : α → β} (u : ultrafilter β) (inj : function.injective m) (large : set.range m ∈ u) :
ultrafilter α

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

Equations
source
@[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
source
@[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
source
@[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
source
@[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₂
source
@[protected, instance]
def ultrafilter.has_pure  :
has_pure ultrafilter

The principal ultrafilter associated to a point x.

Equations
source
@[simp]
theorem ultrafilter.mem_pure {α : Type u} {a : α} {s : set α} :
s ∈ has_pure.pure a ↔ a ∈ s
source
@[simp]
theorem ultrafilter.coe_pure {α : Type u} (a : α) :
↑(has_pure.pure a) = has_pure.pure a
source
@[simp]
theorem ultrafilter.map_pure {α : Type u} {β : Type v} (m : α → β) (a : α) :
ultrafilter.map m (has_pure.pure a) = has_pure.pure (m a)
source
@[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
source
theorem ultrafilter.pure_injective {α : Type u} :
function.injective has_pure.pure
source
@[protected, instance]
def ultrafilter.inhabited {α : Type u} [inhabited α] :
inhabited (ultrafilter α)
Equations
source
@[protected, instance]
def ultrafilter.nonempty {α : Type u} [nonempty α] :
nonempty (ultrafilter α)
source
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
source
theorem ultrafilter.eq_pure_of_finite {α : Type u} [finite α] (f : ultrafilter α) :
∃ (a : α), f = has_pure.pure a
source
theorem ultrafilter.le_cofinite_or_eq_pure {α : Type u} (f : ultrafilter α) :
↑f ≤ filter.cofinite ∨ ∃ (a : α), f = has_pure.pure a
source
def ultrafilter.bind {α : Type u} {β : Type v} (f : ultrafilter α) (m : α → ultrafilter β) :
ultrafilter β

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

Equations
source
@[protected, instance]
def ultrafilter.has_bind  :
has_bind ultrafilter
Equations
source
@[protected, instance]
def ultrafilter.functor  :
functor ultrafilter
Equations
source
@[protected, instance]
def ultrafilter.monad  :
monad ultrafilter
Equations
source
@[protected, instance]
def ultrafilter.is_lawful_monad  :
is_lawful_monad ultrafilter
source
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.

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

Alias of ultrafilter.exists_le.

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

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
source
theorem ultrafilter.of_le {α : Type u} (f : filter α) [f.ne_bot] :
↑(ultrafilter.of f) ≤ f
source
theorem ultrafilter.of_coe {α : Type u} (f : ultrafilter α) :
ultrafilter.of ↑f = f
source
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
source
theorem filter.is_atom_pure {α : Type u} {a : α} :
is_atom (has_pure.pure a)
source
@[protected]
theorem filter.ne_bot.le_pure_iff {α : Type u} {f : filter α} {a : α} (hf : f.ne_bot) :
f ≤ has_pure.pure a ↔ f = has_pure.pure a
source
@[simp]
theorem filter.lt_pure_iff {α : Type u} {f : filter α} {a : α} :
f < has_pure.pure a ↔ f = ⊥
source
theorem filter.le_pure_iff' {α : Type u} {f : filter α} {a : α} :
f ≤ has_pure.pure a ↔ f = ⊥ ∨ f = has_pure.pure a
source
@[simp]
theorem filter.Iic_pure {α : Type u} (a : α) :
set.Iic (has_pure.pure a) = {⊥, has_pure.pure a}
source
theorem filter.mem_iff_ultrafilter {α : Type u} {f : filter α} {s : set α} :
s ∈ f ↔ ∀ (g : ultrafilter α), ↑g ≤ f → s ∈ g
source
theorem filter.le_iff_ultrafilter {α : Type u} {f₁ f₂ : filter α} :
f₁ ≤ f₂ ↔ ∀ (g : ultrafilter α), ↑g ≤ f₁ → ↑g ≤ f₂
source
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.

source
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.

source
theorem filter.exists_ultrafilter_iff {α : Type u} {f : filter α} :
(∃ (u : ultrafilter α), ↑u ≤ f) ↔ f.ne_bot
source
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
source
noncomputable def filter.hyperfilter (α : Type u) [infinite α] :
ultrafilter α

The ultrafilter extending the cofinite filter.

Equations
source
theorem filter.hyperfilter_le_cofinite {α : Type u} [infinite α] :
↑(filter.hyperfilter α) ≤ filter.cofinite
source
@[simp]
theorem filter.bot_ne_hyperfilter {α : Type u} [infinite α] :
⊥ ≠ ↑(filter.hyperfilter α)
source
theorem filter.nmem_hyperfilter_of_finite {α : Type u} [infinite α] {s : set α} (hf : s.finite) :
s ∉ filter.hyperfilter α
source
theorem set.finite.nmem_hyperfilter {α : Type u} [infinite α] {s : set α} (hf : s.finite) :
s ∉ filter.hyperfilter α

Alias of filter.nmem_hyperfilter_of_finite.

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

Alias of filter.compl_mem_hyperfilter_of_finite.

source
theorem filter.mem_hyperfilter_of_finite_compl {α : Type u} [infinite α] {s : set α} (hf : sᶜ.finite) :
s ∈ filter.hyperfilter α
source
theorem ultrafilter.comap_inf_principal_ne_bot_of_image_mem {α : Type u} {β : Type v} {m : α → β} {s : set α} {g : ultrafilter β} (h : m '' s ∈ g) :
(filter.comap m ↑g ⊓ filter.principal s).ne_bot
source
noncomputable def ultrafilter.of_comap_inf_principal {α : Type u} {β : Type v} {m : α → β} {s : set α} {g : ultrafilter β} (h : m '' s ∈ g) :
ultrafilter α

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

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