Mathlib.Order.Filter.Ultrafilter.Basic

Ultrafilter.finite_sUnion_mem_iff theorem

{s : Set (Set α)} (hs : s.Finite) : ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f

Full source

theorem finite_sUnion_mem_iff {s : Set (Set α)} (hs : s.Finite) : ⋃₀ s⋃₀ s ∈ f⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f := by
  induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ his => simp [union_mem_iff, his, or_and_right, exists_or]

Ultrafilter Membership Criterion for Finite Unions

Informal description

Let $s$ be a finite collection of subsets of a type $\alpha$. For any ultrafilter $f$ on $\alpha$, the union $\bigcup₀ s$ belongs to $f$ if and only if there exists a subset $t \in s$ such that $t$ belongs to $f$.

Ultrafilter.finite_biUnion_mem_iff theorem

{is : Set β} {s : β → Set α} (his : is.Finite) : (⋃ i ∈ is, s i) ∈ f ↔ ∃ i ∈ is, s i ∈ f

Full source

theorem finite_biUnion_mem_iff {is : Set β} {s : β → Set α} (his : is.Finite) :
    (⋃ i ∈ is, s i) ∈ f(⋃ i ∈ is, s i) ∈ f ↔ ∃ i ∈ is, s i ∈ f := by
  simp only [← sUnion_image, finite_sUnion_mem_iff (his.image s), exists_mem_image]

Ultrafilter Membership Criterion for Finite Indexed Unions

Informal description

Let $I$ be a finite set and $\{S_i\}_{i \in I}$ be a family of subsets of a type $\alpha$. For any ultrafilter $f$ on $\alpha$, the union $\bigcup_{i \in I} S_i$ belongs to $f$ if and only if there exists some $i \in I$ such that $S_i \in f$.

Ultrafilter.eventually_exists_mem_iff theorem

 {is : Set β} {P : β → α → Prop} (his : is.Finite) : (∀ᶠ i in f, ∃ a ∈ is, P a i) ↔ ∃ a ∈ is, ∀ᶠ i in f, P a i

Full source

lemma eventually_exists_mem_iff {is : Set β} {P : β → α → Prop} (his : is.Finite) :
    (∀ᶠ i in f, ∃ a ∈ is, P a i) ↔ ∃ a ∈ is, ∀ᶠ i in f, P a i := by
  simp only [Filter.Eventually, Ultrafilter.mem_coe]
  convert f.finite_biUnion_mem_iff his (s := P) with i
  aesop

Ultrafilter Finite Existential Quantifier Criterion

Informal description

Let $I$ be a finite set and $P : I \times \alpha \to \text{Prop}$ be a predicate. For any ultrafilter $f$ on $\alpha$, the following are equivalent: 1. For almost all $x$ in $f$, there exists $a \in I$ such that $P(a, x)$ holds. 2. There exists $a \in I$ such that for almost all $x$ in $f$, $P(a, x)$ holds. Here "for almost all $x$ in $f$" means that the set of $x$ satisfying the condition belongs to $f$.

Ultrafilter.eventually_exists_iff theorem

[Finite β] {P : β → α → Prop} : (∀ᶠ i in f, ∃ a, P a i) ↔ ∃ a, ∀ᶠ i in f, P a i

Full source

lemma eventually_exists_iff [Finite β] {P : β → α → Prop} :
    (∀ᶠ i in f, ∃ a, P a i) ↔ ∃ a, ∀ᶠ i in f, P a i := by
  simpa using eventually_exists_mem_iff (f := f) (P := P) Set.finite_univ

Ultrafilter Finite Existential Quantifier Equivalence

Informal description

Let $\beta$ be a finite type and $P : \beta \times \alpha \to \text{Prop}$ be a predicate. For any ultrafilter $f$ on $\alpha$, the following are equivalent: 1. For almost all $x$ in $f$, there exists $a \in \beta$ such that $P(a, x)$ holds. 2. There exists $a \in \beta$ such that for almost all $x$ in $f$, $P(a, x)$ holds. Here "for almost all $x$ in $f$" means that the set of $x$ satisfying the condition belongs to $f$.

Ultrafilter.le_cofinite_or_eq_pure theorem

(f : Ultrafilter α) : (f : Filter α) ≤ cofinite ∨ ∃ a, f = pure a

Full source

theorem le_cofinite_or_eq_pure (f : Ultrafilter α) : (f : Filter α) ≤ cofinite ∨ ∃ a, f = pure a :=
  or_iff_not_imp_left.2 fun h =>
    let ⟨_, hs, hfin⟩ := Filter.disjoint_cofinite_right.1 (disjoint_iff_not_le.2 h)
    let ⟨a, _, hf⟩ := eq_pure_of_finite_mem hfin hs
    ⟨a, hf⟩

Ultrafilter Classification: Cofinite or Principal

Informal description

For any ultrafilter $f$ on a type $\alpha$, either $f$ contains all cofinite sets (i.e., $f$ is finer than the cofinite filter) or there exists an element $a \in \alpha$ such that $f$ is the principal ultrafilter generated by $a$.

Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty theorem

 (S : Set (Set α)) (cond : ∀ T : Finset (Set α), (↑T : Set (Set α)) ⊆ S → (⋂₀ (↑T : Set (Set α))).Nonempty) :
  ∃ F : Ultrafilter α, S ⊆ F.sets

Full source

theorem exists_ultrafilter_of_finite_inter_nonempty (S : Set (Set α))
    (cond : ∀ T : Finset (Set α), (↑T : Set (Set α)) ⊆ S → (⋂₀ (↑T : Set (Set α))).Nonempty) :
    ∃ F : Ultrafilter α, S ⊆ F.sets :=
  haveI : NeBot (generate S) :=
    generate_neBot_iff.2 fun _ hts ht =>
      ht.coe_toFinset ▸ cond ht.toFinset (ht.coe_toFinset.symm ▸ hts)
  ⟨of (generate S), fun _ ht => (of_le <| generate S) <| GenerateSets.basic ht⟩

Existence of Ultrafilter Extending a Family with Finite Intersection Property

Informal description

Let $S$ be a collection of subsets of a type $\alpha$ such that for every finite subset $T \subseteq S$, the intersection $\bigcap T$ is nonempty. Then there exists an ultrafilter $F$ on $\alpha$ such that $S \subseteq F$.

Filter.atTop_eq_pure_of_isTop theorem

[PartialOrder α] {x : α} (hx : IsTop x) : (atTop : Filter α) = pure x

Full source

lemma atTop_eq_pure_of_isTop [PartialOrder α] {x : α} (hx : IsTop x) :
    (atTop : Filter α) = pure x :=
  {top := x, le_top := hx : OrderTop α}.atTop_eq

Characterization of `atTop` Filter for Partial Order with Top Element

Informal description

Let $\alpha$ be a partially ordered set. If $x$ is a top element of $\alpha$, then the filter `atTop` on $\alpha$ is equal to the principal filter generated by $x$, i.e., $\text{atTop} = \text{pure } x$.

Filter.atBot_eq_pure_of_isBot theorem

[PartialOrder α] {x : α} (hx : IsBot x) : (atBot : Filter α) = pure x

Full source

lemma atBot_eq_pure_of_isBot [PartialOrder α] {x : α} (hx : IsBot x) :
    (atBot : Filter α) = pure x :=
  @atTop_eq_pure_of_isTop αᵒᵈ _ _ hx

Characterization of `atBot` Filter for Partial Order with Bottom Element

Informal description

Let $\alpha$ be a partially ordered set. If $x$ is a bottom element of $\alpha$, then the filter `atBot` on $\alpha$ is equal to the principal filter generated by $x$, i.e., $\text{atBot} = \text{pure } x$.

Filter.tendsto_iff_ultrafilter theorem

 (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Tendsto f l₁ l₂ ↔ ∀ g : Ultrafilter α, ↑g ≤ l₁ → Tendsto f g l₂

Full source

/-- The `tendsto` relation can be checked on ultrafilters. -/
theorem tendsto_iff_ultrafilter (f : α → β) (l₁ : Filter α) (l₂ : Filter β) :
    TendstoTendsto f l₁ l₂ ↔ ∀ g : Ultrafilter α, ↑g ≤ l₁ → Tendsto f g l₂ := by
  simpa only [tendsto_iff_comap] using le_iff_ultrafilter

Ultrafilter Characterization of Tendsto: $f$ tends to $l_2$ along $l_1$ iff all finer ultrafilters preserve this convergence.

Informal description

For any function $f \colon \alpha \to \beta$ and filters $l_1$ on $\alpha$ and $l_2$ on $\beta$, the function $f$ tends to $l_2$ along $l_1$ if and only if for every ultrafilter $g$ on $\alpha$ such that $g \leq l_1$, the function $f$ tends to $l_2$ along $g$.

Filter.hyperfilter definition

: Ultrafilter α

Full source

/-- The ultrafilter extending the cofinite filter. -/
noncomputable def hyperfilter : Ultrafilter α :=
  Ultrafilter.of cofinite

Hyperfilter (ultrafilter extending the cofinite filter)

Informal description

The hyperfilter on a type $\alpha$ is the ultrafilter extending the cofinite filter, which consists of all subsets of $\alpha$ whose complements are finite. This construction requires $\alpha$ to be infinite to ensure the cofinite filter is non-trivial.

Filter.hyperfilter_le_cofinite theorem

: ↑(hyperfilter α) ≤ @cofinite α

Full source

theorem hyperfilter_le_cofinite : ↑(hyperfilter α) ≤ @cofinite α :=
  Ultrafilter.of_le cofinite

Hyperfilter is Finer than Cofinite Filter

Informal description

For any type $\alpha$, the hyperfilter (an ultrafilter extending the cofinite filter) is contained in the cofinite filter, i.e., $\text{hyperfilter}(\alpha) \leq \text{cofinite}(\alpha)$.

Nat.hyperfilter_le_atTop theorem

: (hyperfilter ℕ).toFilter ≤ atTop

Full source

theorem _root_.Nat.hyperfilter_le_atTop : (hyperfilter ℕ).toFilter ≤ atTop :=
  hyperfilter_le_cofinite.trans_eq Nat.cofinite_eq_atTop

Hyperfilter on Naturals is Finer than `atTop` Filter

Informal description

The hyperfilter on the natural numbers $\mathbb{N}$ is finer than the `atTop` filter, i.e., $\text{hyperfilter}(\mathbb{N}) \leq \text{atTop}$.

Filter.bot_ne_hyperfilter theorem

: (⊥ : Filter α) ≠ hyperfilter α

Full source

@[simp]
theorem bot_ne_hyperfilter : (⊥ : Filter α) ≠ hyperfilter α :=
  (NeBot.ne inferInstance).symm

Hyperfilter is Nontrivial

Informal description

For any type $\alpha$, the trivial (bottom) filter on $\alpha$ is not equal to the hyperfilter on $\alpha$.

Filter.nmem_hyperfilter_of_finite theorem

{s : Set α} (hf : s.Finite) : s ∉ hyperfilter α

Full source

theorem nmem_hyperfilter_of_finite {s : Set α} (hf : s.Finite) : s ∉ hyperfilter α := fun hy =>
  compl_not_mem hy <| hyperfilter_le_cofinite hf.compl_mem_cofinite

Finite Sets Excluded from Hyperfilter

Informal description

For any finite subset $s$ of an infinite type $\alpha$, the set $s$ does not belong to the hyperfilter on $\alpha$.

Filter.compl_mem_hyperfilter_of_finite theorem

{s : Set α} (hf : Set.Finite s) : sᶜ ∈ hyperfilter α

Full source

theorem compl_mem_hyperfilter_of_finite {s : Set α} (hf : Set.Finite s) : sᶜsᶜ ∈ hyperfilter α :=
  compl_mem_iff_not_mem.2 hf.nmem_hyperfilter

Complement of Finite Set Belongs to Hyperfilter

Informal description

For any finite subset $s$ of an infinite type $\alpha$, the complement of $s$ belongs to the hyperfilter on $\alpha$.

Filter.mem_hyperfilter_of_finite_compl theorem

{s : Set α} (hf : Set.Finite sᶜ) : s ∈ hyperfilter α

Full source

theorem mem_hyperfilter_of_finite_compl {s : Set α} (hf : Set.Finite sᶜ) : s ∈ hyperfilter α :=
  compl_compl s ▸ hf.compl_mem_hyperfilter

Membership in Hyperfilter via Finite Complement: $s^c$ finite $\Rightarrow$ $s \in \text{hyperfilter}$

Informal description

For any subset $s$ of an infinite type $\alpha$, if the complement of $s$ is finite, then $s$ belongs to the hyperfilter on $\alpha$.