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} : IsAtomic (Filter α)

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

structure Ultrafilter (α : Type u_2) extends Filter α : 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).sets → x ⊆ y → y ∈ (↑self).sets
• inter_sets {x y : Set α} : x ∈ (↑self).sets → y ∈ (↑self).sets → x ∩ y ∈ (↑self).sets
• neBot' : (↑self).NeBot

  An ultrafilter is nontrivial.

• le_of_le (g : Filter α) : g.NeBot → g ≤ ↑self → ↑self ≤ 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.

instance Ultrafilter.instCoeTCFilter {α : Type u} : CoeTC (Ultrafilter α) (Filter α)

Equations

• Ultrafilter.instCoeTCFilter = { coe := Ultrafilter.toFilter }

instance Ultrafilter.instMembershipSet {α : Type u} : Membership (Set α) (Ultrafilter α)

Equations

• Ultrafilter.instMembershipSet = { mem := fun (f : Ultrafilter α) (s : Set α) => s ∈ ↑f }

theorem Ultrafilter.unique {α : Type u} (f : Ultrafilter α) {g : Filter α} (h : g ≤ ↑f) (hne : g.NeBot := by infer_instance) : g = ↑f

instance Ultrafilter.neBot {α : Type u} (f : Ultrafilter α) : (↑f).NeBot

theorem Ultrafilter.isAtom {α : Type u} (f : Ultrafilter α) : IsAtom ↑f

@[simp]

theorem Ultrafilter.mem_coe {α : Type u} {f : Ultrafilter α} {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 : Ultrafilter α} (h : ↑f ≤ ↑g) : f = g

@[simp]

theorem Ultrafilter.coe_le_coe {α : Type u} {f g : Ultrafilter α} : ↑f ≤ ↑g ↔ f = g

@[simp]

theorem Ultrafilter.coe_inj {α : Type u} {f g : Ultrafilter α} : ↑f = ↑g ↔ f = g

theorem Ultrafilter.ext {α : Type u} ⦃f g : Ultrafilter α⦄ (h : ∀ (s : Set α), s ∈ f ↔ s ∈ g) : f = g

theorem Ultrafilter.le_of_inf_neBot {α : Type u} (f : Ultrafilter α) {g : Filter α} (hg : (↑f ⊓ g).NeBot) : ↑f ≤ g

theorem Ultrafilter.le_of_inf_neBot' {α : Type u} (f : Ultrafilter α) {g : Filter α} (hg : (g ⊓ ↑f).NeBot) : ↑f ≤ g

theorem Ultrafilter.inf_neBot_iff {α : Type u} {f : Ultrafilter α} {g : Filter α} : (↑f ⊓ g).NeBot ↔ ↑f ≤ g

theorem Ultrafilter.disjoint_iff_not_le {α : Type u} {f : Ultrafilter α} {g : Filter α} : Disjoint (↑f) g ↔ ¬↑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 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.ofComplNotMemIff {α : 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

• Ultrafilter.ofComplNotMemIff f h = { toFilter := f, neBot' := ⋯, le_of_le := ⋯ }

def Ultrafilter.ofAtom {α : Type u} (f : Filter α) (hf : IsAtom f) : Ultrafilter α

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

Equations

• Ultrafilter.ofAtom f hf = { toFilter := f, neBot' := ⋯, le_of_le := ⋯ }

theorem Ultrafilter.nonempty_of_mem {α : Type u} {f : Ultrafilter α} {s : Set α} (hs : s ∈ f) : s.Nonempty

theorem Ultrafilter.ne_empty_of_mem {α : Type u} {f : Ultrafilter α} {s : Set α} (hs : s ∈ f) : s ≠ ∅

@[simp]

theorem Ultrafilter.empty_not_mem {α : Type u} {f : Ultrafilter α} : ∅ ∉ f

@[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

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 ∈ s, t ∈ f

theorem Ultrafilter.finite_biUnion_mem_iff {α : Type u} {β : Type v} {f : Ultrafilter α} {is : Set β} {s : β → Set α} (his : is.Finite) : ⋃ i ∈ is, s i ∈ f ↔ ∃ i ∈ is, s i ∈ f

theorem Ultrafilter.eventually_exists_mem_iff {α : Type u} {β : Type v} {f : Ultrafilter α} {is : Set β} {P : β → α → Prop} (his : is.Finite) : (∀ᶠ (i : α) in ↑f, ∃ a ∈ is, P a i) ↔ ∃ a ∈ is, ∀ᶠ (i : α) in ↑f, P a i

theorem Ultrafilter.eventually_exists_iff {α : Type u} {β : Type v} {f : Ultrafilter α} [Finite β] {P : β → α → Prop} : (∀ᶠ (i : α) in ↑f, ∃ (a : β), P a i) ↔ ∃ (a : β), ∀ᶠ (i : α) in ↑f, P a i

def Ultrafilter.map {α : Type u} {β : Type v} (m : α → β) (f : Ultrafilter α) : Ultrafilter β

Pushforward for ultrafilters.

Equations

• Ultrafilter.map m f = Ultrafilter.ofComplNotMemIff (Filter.map m ↑f) ⋯

@[simp]

theorem Ultrafilter.coe_map {α : Type u} {β : Type v} (m : α → β) (f : Ultrafilter α) : ↑(Ultrafilter.map m f) = Filter.map m ↑f

@[simp]

theorem Ultrafilter.mem_map {α : Type u} {β : Type v} {m : α → β} {f : Ultrafilter α} {s : Set β} : s ∈ Ultrafilter.map m f ↔ m ⁻¹' s ∈ f

@[simp]

theorem Ultrafilter.map_id {α : Type u} (f : Ultrafilter α) : Ultrafilter.map id f = f

@[simp]

theorem Ultrafilter.map_id' {α : Type u} (f : Ultrafilter α) : Ultrafilter.map (fun (x : α) => x) f = f

@[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

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

• u.comap inj large = { toFilter := Filter.comap m ↑u, neBot' := ⋯, le_of_le := ⋯ }

@[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

@[simp]

theorem Ultrafilter.comap_id {α : Type u} (f : Ultrafilter α) (h₀ : 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₂

instance Ultrafilter.instPure : Pure Ultrafilter

The principal ultrafilter associated to a point x.

Equations

• Ultrafilter.instPure = { pure := fun {α : Type ?u.6} (a : α) => Ultrafilter.ofComplNotMemIff (pure a) ⋯ }

@[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 : α) : Ultrafilter.map m (pure a) = pure (m a)

@[simp]

theorem Ultrafilter.comap_pure {α : Type u} {β : Type v} {m : α → β} (a : α) (inj : Function.Injective m) (large : Set.range m ∈ pure (m a)) : (pure (m a)).comap inj large = pure a

theorem Ultrafilter.pure_injective {α : Type u} : Function.Injective pure

instance Ultrafilter.instInhabited {α : Type u} [Inhabited α] : Inhabited (Ultrafilter α)

Equations

• Ultrafilter.instInhabited = { default := pure default }

instance Ultrafilter.instNonempty {α : Type u} [Nonempty α] : Nonempty (Ultrafilter α)

theorem Ultrafilter.eq_pure_of_finite_mem {α : Type u} {f : Ultrafilter α} {s : Set α} (h : s.Finite) (h' : s ∈ f) : ∃ x ∈ s, f = pure x

theorem Ultrafilter.eq_pure_of_finite {α : Type u} [Finite α] (f : Ultrafilter α) : ∃ (a : α), f = pure a

theorem Ultrafilter.le_cofinite_or_eq_pure {α : Type u} (f : Ultrafilter α) : ↑f ≤ Filter.cofinite ∨ ∃ (a : α), f = pure a

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

• f.bind m = Ultrafilter.ofComplNotMemIff ((↑f).bind fun (x : α) => ↑(m x)) ⋯

instance Ultrafilter.instBind : Bind Ultrafilter

Equations

• Ultrafilter.instBind = { bind := @Ultrafilter.bind }

instance Ultrafilter.functor : Functor Ultrafilter

Equations

• Ultrafilter.functor = { map := @Ultrafilter.map, mapConst := fun {α β : Type ?u.8} => Ultrafilter.map ∘ Function.const β }

instance Ultrafilter.monad : Monad Ultrafilter

Equations

• Ultrafilter.monad = Monad.mk

instance Ultrafilter.lawfulMonad : LawfulMonad Ultrafilter

theorem Ultrafilter.exists_le {α : Type u} (f : Filter α) [h : f.NeBot] : ∃ (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.NeBot] : ∃ (u : Ultrafilter α), ↑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 : Filter α) [f.NeBot] : 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

• Ultrafilter.of f = Classical.choose ⋯

theorem Ultrafilter.of_le {α : Type u} (f : Filter α) [f.NeBot] : ↑(Ultrafilter.of f) ≤ f

theorem Ultrafilter.of_coe {α : Type u} (f : Ultrafilter α) : Ultrafilter.of ↑f = f

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).sets

theorem Filter.isAtom_pure {α : Type u} {a : α} : IsAtom (pure a)

theorem Filter.NeBot.le_pure_iff {α : Type u} {f : Filter α} {a : α} (hf : f.NeBot) : f ≤ pure a ↔ f = pure a

theorem Filter.NeBot.eq_pure_iff {α : Type u} {f : Filter α} (hf : f.NeBot) {x : α} : f = pure x ↔ {x} ∈ f

theorem Filter.atTop_eq_pure_of_isTop {α : Type u} [LinearOrder α] {x : α} (hx : IsTop x) : Filter.atTop = pure x

theorem Filter.atBot_eq_pure_of_isBot {α : Type u} [LinearOrder α] {x : α} (hx : IsBot x) : Filter.atBot = pure x

@[simp]

theorem Filter.lt_pure_iff {α : Type u} {f : Filter α} {a : α} : f < pure a ↔ f = ⊥

theorem Filter.le_pure_iff' {α : Type u} {f : Filter α} {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 : 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.iSup_ultrafilter_le_eq {α : Type u} (f : Filter α) : ⨆ (g : Ultrafilter α), ⨆ (_ : ↑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.NeBot

theorem Filter.forall_neBot_le_iff {α : Type u} {g : Filter α} {p : Filter α → Prop} (hp : Monotone p) : (∀ (f : Filter α), f.NeBot → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f

noncomputable def Filter.hyperfilter (α : Type u) [Infinite α] : Ultrafilter α

The ultrafilter extending the cofinite filter.

Equations

• Filter.hyperfilter α = Ultrafilter.of Filter.cofinite

theorem Filter.hyperfilter_le_cofinite {α : Type u} [Infinite α] : ↑(Filter.hyperfilter α) ≤ Filter.cofinite

theorem Nat.hyperfilter_le_atTop : ↑(Filter.hyperfilter ℕ) ≤ Filter.atTop

@[simp]

theorem Filter.bot_ne_hyperfilter {α : Type u} [Infinite α] : ⊥ ≠ ↑(Filter.hyperfilter α)

theorem Filter.nmem_hyperfilter_of_finite {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) : s ∉ Filter.hyperfilter α

theorem Set.Finite.nmem_hyperfilter {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) : s ∉ Filter.hyperfilter α

Alias of Filter.nmem_hyperfilter_of_finite.

theorem Filter.compl_mem_hyperfilter_of_finite {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) : sᶜ ∈ Filter.hyperfilter α

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.

theorem Filter.mem_hyperfilter_of_finite_compl {α : Type u} [Infinite α] {s : Set α} (hf : sᶜ.Finite) : s ∈ Filter.hyperfilter α

theorem Ultrafilter.comap_inf_principal_neBot_of_image_mem {α : Type u} {β : Type v} {m : α → β} {s : Set α} {g : Ultrafilter β} (h : m '' s ∈ g) : (Filter.comap m ↑g ⊓ Filter.principal s).NeBot

noncomputable def Ultrafilter.ofComapInfPrincipal {α : 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

• Ultrafilter.ofComapInfPrincipal h = Ultrafilter.of (Filter.comap m ↑g ⊓ Filter.principal s)

theorem Ultrafilter.ofComapInfPrincipal_mem {α : Type u} {β : Type v} {m : α → β} {s : Set α} {g : Ultrafilter β} (h : m '' s ∈ g) : s ∈ Ultrafilter.ofComapInfPrincipal h

theorem Ultrafilter.ofComapInfPrincipal_eq_of_map {α : Type u} {β : Type v} {m : α → β} {s : Set α} {g : Ultrafilter β} (h : m '' s ∈ g) : Ultrafilter.map m (Ultrafilter.ofComapInfPrincipal h) = g

theorem Ultrafilter.eq_of_le_pure {X : Type u_2} {α : Filter X} (hα : α.NeBot) {x y : X} (hx : α ≤ pure x) (hy : α ≤ pure y) : x = y