Ultrafilters

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

• hyperfilter: the ultrafilter extending the cofinite filter.

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

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

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.atTop_eq_pure_of_isTop {α : Type u} [LinearOrder α] {x : α} (hx : IsTop x) : atTop = pure x

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

theorem Filter.tendsto_iff_ultrafilter {α : Type u} {β : Type v} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → Tendsto f (↑g) l₂

The tendsto relation can be checked on ultrafilters.

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 α] : ↑(hyperfilter α) ≤ cofinite

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

@[simp]

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

theorem Filter.nmem_hyperfilter_of_finite {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) : s ∉ 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ᶜ ∈ 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 ∈ hyperfilter α