Ultrafilters #

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

• Ultrafilter.of: an ultrafilter that is less than or equal to a given filter;
• Ultrafilter: subtype of ultrafilters;
• pure x : Ultrafilter α: pure x as an Ultrafilter;
• Ultrafilter.map, Ultrafilter.bind, Ultrafilter.comap : operations on ultrafilters;
• hyperfilter: the ultrafilter extending the cofinite filter.
instance instIsAtomicFilter {α : Type u} :

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

Equations
• =
structure Ultrafilter (α : Type u_2) extends :
Type u_2

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

• sets : Set (Set α)
• univ_sets : Set.univ (↑self).sets
• sets_of_superset : ∀ {x y : Set α}, x (↑self).setsx yy (↑self).sets
• inter_sets : ∀ {x y : Set α}, x (↑self).setsy (↑self).setsx y (↑self).sets
• neBot' : (↑self).NeBot

An ultrafilter is nontrivial.

• le_of_le : ∀ (g : ), g.NeBotg selfself g

If g is a nontrivial filter that is less than or equal to an ultrafilter, then it is greater than or equal to the ultrafilter.

Instances For
theorem Ultrafilter.neBot' {α : Type u_2} (self : ) :
(↑self).NeBot

An ultrafilter is nontrivial.

theorem Ultrafilter.le_of_le {α : Type u_2} (self : ) (g : ) :
g.NeBotg selfself g

If g is a nontrivial filter that is less than or equal to an ultrafilter, then it is greater than or equal to the ultrafilter.

Equations
• Ultrafilter.instCoeTCFilter = { coe := Ultrafilter.toFilter }
Equations
• Ultrafilter.instMembershipSet = { mem := fun (f : ) (s : Set α) => s f }
theorem Ultrafilter.unique {α : Type u} (f : ) {g : } (h : g f) (hne : autoParam g.NeBot _auto✝) :
g = f
instance Ultrafilter.neBot {α : Type u} (f : ) :
(↑f).NeBot
Equations
• =
theorem Ultrafilter.isAtom {α : Type u} (f : ) :
IsAtom f
@[simp]
theorem Ultrafilter.mem_coe {α : Type u} {f : } {s : Set α} :
s f s f
theorem Ultrafilter.coe_injective {α : Type u} :
Function.Injective Ultrafilter.toFilter
theorem Ultrafilter.eq_of_le {α : Type u} {f : } {g : } (h : f g) :
f = g
@[simp]
theorem Ultrafilter.coe_le_coe {α : Type u} {f : } {g : } :
f g f = g
@[simp]
theorem Ultrafilter.coe_inj {α : Type u} {f : } {g : } :
f = g f = g
theorem Ultrafilter.ext_iff {α : Type u} {f : } {g : } :
f = g ∀ (s : Set α), s f s g
theorem Ultrafilter.ext {α : Type u} ⦃f : ⦃g : (h : ∀ (s : Set α), s f s g) :
f = g
theorem Ultrafilter.le_of_inf_neBot {α : Type u} (f : ) {g : } (hg : (f g).NeBot) :
f g
theorem Ultrafilter.le_of_inf_neBot' {α : Type u} (f : ) {g : } (hg : (g f).NeBot) :
f g
theorem Ultrafilter.inf_neBot_iff {α : Type u} {f : } {g : } :
(f g).NeBot f g
theorem Ultrafilter.disjoint_iff_not_le {α : Type u} {f : } {g : } :
Disjoint (↑f) g ¬f g
@[simp]
theorem Ultrafilter.compl_not_mem_iff {α : Type u} {f : } {s : Set α} :
sf s f
@[simp]
theorem Ultrafilter.frequently_iff_eventually {α : Type u} {f : } {p : αProp} :
(∃ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, p x
theorem Filter.Frequently.eventually {α : Type u} {f : } {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 : } {s : Set α} :
s f sf
theorem Ultrafilter.diff_mem_iff {α : Type u} {s : Set α} {t : Set α} (f : ) :
s \ t f s f tf
def Ultrafilter.ofComplNotMemIff {α : Type u} (f : ) (h : ∀ (s : Set α), sf s f) :

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

Equations
• = { toFilter := f, neBot' := , le_of_le := }
Instances For
def Ultrafilter.ofAtom {α : Type u} (f : ) (hf : ) :

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

Equations
• = { toFilter := f, neBot' := , le_of_le := }
Instances For
theorem Ultrafilter.nonempty_of_mem {α : Type u} {f : } {s : Set α} (hs : s f) :
s.Nonempty
theorem Ultrafilter.ne_empty_of_mem {α : Type u} {f : } {s : Set α} (hs : s f) :
@[simp]
theorem Ultrafilter.empty_not_mem {α : Type u} {f : } :
f
@[simp]
theorem Ultrafilter.le_sup_iff {α : Type u} {u : } {f : } {g : } :
u f g u f u g
@[simp]
theorem Ultrafilter.union_mem_iff {α : Type u} {f : } {s : Set α} {t : Set α} :
s t f s f t f
theorem Ultrafilter.mem_or_compl_mem {α : Type u} (f : ) (s : Set α) :
s f s f
theorem Ultrafilter.em {α : Type u} (f : ) (p : αProp) :
(∀ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, ¬p x
theorem Ultrafilter.eventually_or {α : Type u} {f : } {p : αProp} {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 : } {p : αProp} :
(∀ᶠ (x : α) in f, ¬p x) ¬∀ᶠ (x : α) in f, p x
theorem Ultrafilter.eventually_imp {α : Type u} {f : } {p : αProp} {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 : } {s : Set (Set α)} (hs : s.Finite) :
⋃₀ s f ts, t f
theorem Ultrafilter.finite_biUnion_mem_iff {α : Type u} {β : Type v} {f : } {is : Set β} {s : βSet α} (his : is.Finite) :
iis, s i f iis, s i f
def Ultrafilter.map {α : Type u} {β : Type v} (m : αβ) (f : ) :

Pushforward for ultrafilters.

Equations
Instances For
@[simp]
theorem Ultrafilter.coe_map {α : Type u} {β : Type v} (m : αβ) (f : ) :
(Ultrafilter.map m f) = Filter.map m f
@[simp]
theorem Ultrafilter.mem_map {α : Type u} {β : Type v} {m : αβ} {f : } {s : Set β} :
s m ⁻¹' s f
@[simp]
theorem Ultrafilter.map_id {α : Type u} (f : ) :
= f
@[simp]
theorem Ultrafilter.map_id' {α : Type u} (f : ) :
Ultrafilter.map (fun (x : α) => x) f = f
@[simp]
theorem Ultrafilter.map_map {α : Type u} {β : Type v} {γ : Type u_1} (f : ) (m : αβ) (n : βγ) :
def Ultrafilter.comap {α : Type u} {β : Type v} {m : αβ} (u : ) (inj : ) (large : u) :

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

Equations
• u.comap inj large = { toFilter := Filter.comap m u, neBot' := , le_of_le := }
Instances For
@[simp]
theorem Ultrafilter.mem_comap {α : Type u} {β : Type v} {m : αβ} (u : ) (inj : ) (large : u) {s : Set α} :
s u.comap inj large m '' s u
@[simp]
theorem Ultrafilter.coe_comap {α : Type u} {β : Type v} {m : αβ} (u : ) (inj : ) (large : u) :
(u.comap inj large) = Filter.comap m u
@[simp]
theorem Ultrafilter.comap_id {α : Type u} (f : ) (h₀ : ) (h₁ : optParam ( f) ) :
f.comap h₀ h₁ = f
@[simp]
theorem Ultrafilter.comap_comap {α : Type u} {β : Type v} {γ : Type u_1} (f : ) {m : αβ} {n : βγ} (inj₀ : ) (large₀ : f) (inj₁ : ) (large₁ : f.comap inj₀ large₀) (inj₂ : optParam (Function.Injective (n m)) ) (large₂ : optParam (Set.range (n m) f) ) :
(f.comap inj₀ large₀).comap inj₁ large₁ = f.comap inj₂ large₂

The principal ultrafilter associated to a point x.

Equations
@[simp]
theorem Ultrafilter.mem_pure {α : Type u} {a : α} {s : Set α} :
s pure a a s
@[simp]
theorem Ultrafilter.coe_pure {α : Type u} (a : α) :
(pure a) = pure a
@[simp]
theorem Ultrafilter.map_pure {α : Type u} {β : Type v} (m : αβ) (a : α) :
@[simp]
theorem Ultrafilter.comap_pure {α : Type u} {β : Type v} {m : αβ} (a : α) (inj : ) (large : pure (m a)) :
(pure (m a)).comap inj large = pure a
instance Ultrafilter.instInhabited {α : Type u} [] :
Equations
• Ultrafilter.instInhabited = { default := pure default }
instance Ultrafilter.instNonempty {α : Type u} [] :
Equations
• =
theorem Ultrafilter.eq_pure_of_finite_mem {α : Type u} {f : } {s : Set α} (h : s.Finite) (h' : s f) :
xs, f = pure x
theorem Ultrafilter.eq_pure_of_finite {α : Type u} [] (f : ) :
∃ (a : α), f = pure a
theorem Ultrafilter.le_cofinite_or_eq_pure {α : Type u} (f : ) :
f Filter.cofinite ∃ (a : α), f = pure a
def Ultrafilter.bind {α : Type u} {β : Type v} (f : ) (m : α) :

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

Equations
Instances For
Equations
Equations
Equations
theorem Ultrafilter.exists_le {α : Type u} (f : ) [h : f.NeBot] :
∃ (u : ), u f

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

theorem Filter.exists_ultrafilter_le {α : Type u} (f : ) [h : f.NeBot] :
∃ (u : ), u f

Alias of Ultrafilter.exists_le.

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

noncomputable def Ultrafilter.of {α : Type u} (f : ) [f.NeBot] :

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
Instances For
theorem Ultrafilter.of_le {α : Type u} (f : ) [f.NeBot] :
f
theorem Ultrafilter.of_coe {α : Type u} (f : ) :
= f
theorem Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty {α : Type u} (S : Set (Set α)) (cond : ∀ (T : Finset (Set α)), T S(⋂₀ T).Nonempty) :
∃ (F : ), S (↑F).sets
theorem Filter.isAtom_pure {α : Type u} {a : α} :
theorem Filter.NeBot.le_pure_iff {α : Type u} {f : } {a : α} (hf : f.NeBot) :
f pure a f = pure a
theorem Filter.NeBot.eq_pure_iff {α : Type u} {f : } (hf : f.NeBot) {x : α} :
f = pure x {x} f
theorem Filter.atTop_eq_pure_of_isTop {α : Type u} [] {x : α} (hx : ) :
Filter.atTop = pure x
theorem Filter.atBot_eq_pure_of_isBot {α : Type u} [] {x : α} (hx : ) :
Filter.atBot = pure x
@[simp]
theorem Filter.lt_pure_iff {α : Type u} {f : } {a : α} :
f < pure a f =
theorem Filter.le_pure_iff' {α : Type u} {f : } {a : α} :
f pure a f = f = pure a
@[simp]
theorem Filter.Iic_pure {α : Type u} (a : α) :
Set.Iic (pure a) = {, pure a}
theorem Filter.mem_iff_ultrafilter {α : Type u} {f : } {s : Set α} :
s f ∀ (g : ), g fs g
theorem Filter.le_iff_ultrafilter {α : Type u} {f₁ : } {f₂ : } :
f₁ f₂ ∀ (g : ), g f₁g f₂
theorem Filter.iSup_ultrafilter_le_eq {α : Type u} (f : ) :
⨆ (g : ), ⨆ (_ : 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₁ : ) (l₂ : ) :
Filter.Tendsto f l₁ l₂ ∀ (g : ), g l₁Filter.Tendsto f (↑g) l₂

The tendsto relation can be checked on ultrafilters.

theorem Filter.exists_ultrafilter_iff {α : Type u} {f : } :
(∃ (u : ), u f) f.NeBot
theorem Filter.forall_neBot_le_iff {α : Type u} {g : } {p : Prop} (hp : ) :
(∀ (f : ), f.NeBotf gp f) ∀ (f : ), f gp f
noncomputable def Filter.hyperfilter (α : Type u) [] :

The ultrafilter extending the cofinite filter.

Equations
Instances For
theorem Filter.hyperfilter_le_cofinite {α : Type u} [] :
Filter.cofinite
theorem Nat.hyperfilter_le_atTop :
Filter.atTop
@[simp]
theorem Filter.bot_ne_hyperfilter {α : Type u} [] :
theorem Filter.nmem_hyperfilter_of_finite {α : Type u} [] {s : Set α} (hf : s.Finite) :
theorem Set.Finite.nmem_hyperfilter {α : Type u} [] {s : Set α} (hf : s.Finite) :

Alias of Filter.nmem_hyperfilter_of_finite.

theorem Filter.compl_mem_hyperfilter_of_finite {α : Type u} [] {s : Set α} (hf : s.Finite) :
theorem Set.Finite.compl_mem_hyperfilter {α : Type u} [] {s : Set α} (hf : s.Finite) :

Alias of Filter.compl_mem_hyperfilter_of_finite.

theorem Filter.mem_hyperfilter_of_finite_compl {α : Type u} [] {s : Set α} (hf : s.Finite) :
theorem Ultrafilter.comap_inf_principal_neBot_of_image_mem {α : Type u} {β : Type v} {m : αβ} {s : Set α} {g : } (h : m '' s g) :
(Filter.comap m g ).NeBot
noncomputable def Ultrafilter.ofComapInfPrincipal {α : Type u} {β : Type v} {m : αβ} {s : Set α} {g : } (h : m '' s g) :

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

Equations
Instances For
theorem Ultrafilter.ofComapInfPrincipal_mem {α : Type u} {β : Type v} {m : αβ} {s : Set α} {g : } (h : m '' s g) :
theorem Ultrafilter.ofComapInfPrincipal_eq_of_map {α : Type u} {β : Type v} {m : αβ} {s : Set α} {g : } (h : m '' s g) :