Filter.Frequently.eventually
theorem Filter.Frequently.eventually :
∀ {α : Type u} {f : Ultrafilter α} {p : α → Prop}, (∃ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, p x
This theorem, named as `Filter.Frequently.eventually`, is an alias for the forward direction of `Ultrafilter.frequently_iff_eventually`. It states that for any type `α`, ultrafilter `f` on `α`, and property `p` of `α`, if there exists frequently an element `x` of type `α` in the ultrafilter `f` that satisfies the property `p`, then it implies that eventually, every element `x` of type `α` in the ultrafilter `f` will satisfy the property `p`. In mathematical terms, if some property `p` holds frequently for elements in an ultrafilter, then eventually that property will hold for all elements in the ultrafilter.
More concisely: If an ultrafilter on a type contains an element satisfying a property frequently, then every element in the ultrafilter eventually satisfies that property.
|
Ultrafilter.le_of_le
theorem Ultrafilter.le_of_le :
∀ {α : Type u_2} (self : Ultrafilter α) (g : Filter α), g.NeBot → g ≤ ↑self → ↑self ≤ g
This theorem states that for any type `α`, if `g` is a nontrivial (not bottom) filter that is less than or equal to an ultrafilter `self`, then it must also be the case that this ultrafilter is less than or equal to the filter `g`. Essentially, in the context of filters, 'less than or equal to' implies equality for a nontrivial filter and an ultrafilter.
More concisely: If `g` is a nontrivial filter and `self` is an ultrafilter, then `g ≤ self` implies `self ≤ g`.
|
Ultrafilter.eq_of_le
theorem Ultrafilter.eq_of_le : ∀ {α : Type u} {f g : Ultrafilter α}, ↑f ≤ ↑g → f = g
This theorem states that for any two ultrafilters `f` and `g` of an arbitrary type `α`, if `f` is less than or equal to `g` (denoted by `↑f ≤ ↑g`), then `f` is equal to `g`. This essentially means that if one ultrafilter's set of elements is a subset of or equal to another's, the two ultrafilters are the same. This is specific to the structure of ultrafilters in set theory.
More concisely: If `f` and `g` are ultrafilters on a set `α`, then `↑f = ↑g` if and only if `f ≤ g`.
|
Filter.tendsto_iff_ultrafilter
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 theorem `Filter.tendsto_iff_ultrafilter` states that for any types `α` and `β`, and for any function `f` from `α` to `β` and any filters `l₁` on `α` and `l₂` on `β`, the function `f` tends to `l₂` along `l₁` if and only if for every ultrafilter `g` on `α`, when `g` is a subset of `l₁`, the function `f` tends to `l₂` along `g`. In other words, the limit of a function at a filter can be checked via ultrafilters contained in that filter.
More concisely: For any functions between types `α` and `β`, a function tends to a filter on `β` along a filter on `α` if and only if it tends to that filter along every ultrafilter contained in the filter on `α`.
|
Ultrafilter.coe_injective
theorem Ultrafilter.coe_injective : ∀ {α : Type u}, Function.Injective Ultrafilter.toFilter
The theorem `Ultrafilter.coe_injective` states that for all types `α`, the function `Ultrafilter.toFilter` is injective. In other words, given any two ultrafilters on a type `α`, if they are mapped to the same filter using `Ultrafilter.toFilter`, then the original ultrafilters must have been the same. This is equivalent to saying that no two distinct ultrafilters on the same type can be mapped to the same filter, ensuring uniqueness of representation in the context of filters.
More concisely: Given any two ultrafilters on the same type, if their images under `Ultrafilter.toFilter` are equal, then the ultrafilters themselves are equal.
|
Filter.isAtom_pure
theorem Filter.isAtom_pure : ∀ {α : Type u} {a : α}, IsAtom (pure a)
The theorem `Filter.isAtom_pure` states that for any type `α` and for any element `a` of type `α`, the pure filter of `a` is an atom. In terms of preorder theory, an atom is an element that is distinct from the bottom element and has no other elements between it and the bottom element. Therefore, in the context of this theorem, the pure filter of `a` is not equivalent to the bottom element, and there are no other filters between it and the bottom filter.
More concisely: For any type `α` and element `a` of type `α`, the pure filter of `a` is a filter atom.
|
Ultrafilter.compl_not_mem_iff
theorem Ultrafilter.compl_not_mem_iff : ∀ {α : Type u} {f : Ultrafilter α} {s : Set α}, sᶜ ∉ f ↔ s ∈ f
This theorem states that for any type `α`, any ultrafilter `f` on `α`, and any set `s` of elements of type `α`, the complement of `s` is not an element of `f` if and only if `s` is an element of `f`. In other words, a set `s` belongs to an ultrafilter `f` if and only if its complement doesn't belong to `f`. This theorem is a basic property of ultrafilters in set theory.
More concisely: An ultrafilter `f` on a type `α` contains a set `s` if and only if it does not contain the complement of `s`.
|
Set.Finite.nmem_hyperfilter
theorem Set.Finite.nmem_hyperfilter :
∀ {α : Type u} [inst : Infinite α] {s : Set α}, s.Finite → s ∉ Filter.hyperfilter α
This theorem, referred to as `Set.Finite.nmem_hyperfilter`, states that for any type `α` which is infinite, and for any set `s` of elements of type `α`, if `s` is finite, then `s` is not a member of the hyperfilter of `α`. In other words, no finite set can belong to the hyperfilter of an infinite type. A hyperfilter is an ultrafilter that extends the cofinite filter on a given type. Note that a finite set is a set with a finite number of elements.
More concisely: For any infinite type `α` and finite set `s` of elements from `α`, `s` is not a member of the hyperfilter of `α`.
|
Nat.hyperfilter_le_atTop
theorem Nat.hyperfilter_le_atTop : ↑(Filter.hyperfilter ℕ) ≤ Filter.atTop
This theorem states that the ultrafilter extension of the cofinite filter on natural numbers (`Filter.hyperfilter ℕ`) is less than or equal to the filter representing the limit towards positive infinity (`Filter.atTop`). In other words, every neighborhood of infinity contains an infinite cofinite set. This theorem is about the inclusion relationship between these two filters in the natural numbers context.
More concisely: The cofinite ultrafilter on natural numbers is included in the filter at infinity.
|
Ultrafilter.coe_map
theorem Ultrafilter.coe_map :
∀ {α : Type u} {β : Type v} (m : α → β) (f : Ultrafilter α), ↑(Ultrafilter.map m f) = Filter.map m ↑f
This theorem states that for any function `m` from type `α` to type `β` and any ultrafilter `f` of type `α`, the result of mapping `m` over `f` and then casting it to a filter (`↑(Ultrafilter.map m f)`) is the same as first casting `f` to a filter and then mapping `m` over it (`Filter.map m ↑f`). In other words, it confirms that the operations of mapping a function over an ultrafilter and casting to a filter can be performed in either order without affecting the outcome.
More concisely: For any function `m` and ultrafilter `f`, `Ultrafilter.map m (Ultrafilter.ofFilter (Filter.map m ( Filter.lift f )))` equals `Filter.map m f`.
|
Ultrafilter.unique
theorem Ultrafilter.unique :
∀ {α : Type u} (f : Ultrafilter α) {g : Filter α}, g ≤ ↑f → autoParam g.NeBot _auto✝ → g = ↑f
The theorem `Ultrafilter.unique` states that for any type `α`, given an ultrafilter `f` of type `α`, and any other filter `g` on `α` that is less than or equal to `f` and is not the bottom filter (as mandated by the `autoParam` gadget), then `g` has to be equal to `f`. In other words, this theorem is about the uniqueness of ultrafilters: if there is a filter that is not the bottom filter and is included in an ultrafilter, then they have to be the same.
More concisely: For any type `α` and ultrafilter `f` on `α`, if there exists a filter `g` on `α` that is strictly below `f` and not the bottom filter, then `g = f`.
|
Ultrafilter.exists_le
theorem Ultrafilter.exists_le : ∀ {α : Type u} (f : Filter α) [h : f.NeBot], ∃ u, ↑u ≤ f
The Ultrafilter Lemma states that for any given non-zero (or proper) filter `f` over a type `α`, there exists an ultrafilter `u` such that `u` is a superset of `f`. In other words, any proper filter is included in an ultrafilter.
More concisely: For every non-zero filter `f` over a type `α`, there exists an ultrafilter `u` containing `f`.
|
Mathlib.Order.Filter.Ultrafilter._auxLemma.1
theorem Mathlib.Order.Filter.Ultrafilter._auxLemma.1 :
∀ {α : Type u} {f : Ultrafilter α} {s : Set α}, (s ∈ ↑f) = (s ∈ f)
This theorem states that for any type `α`, any ultrafilter `f` of type `α`, and any set `s` of type `α`, the membership of the set `s` in the coercion of the ultrafilter `f` is equivalent to the membership of the set `s` in the ultrafilter `f` itself. In other words, the set `s` is a member of the ultrafilter `f` if and only if `s` is also a member of the ultrafilter `f` after it has been coerced.
More concisely: For any ultrafilter `f` on type `α` and any set `s` of type `α`, the set `s` is in the ultrafilter `f` if and only if `s` is in the coercion of `f`.
|
Ultrafilter.le_of_inf_neBot
theorem Ultrafilter.le_of_inf_neBot : ∀ {α : Type u} (f : Ultrafilter α) {g : Filter α}, (↑f ⊓ g).NeBot → ↑f ≤ g := by
sorry
The theorem `Ultrafilter.le_of_inf_neBot` states that for any type `α`, given an ultrafilter `f` on `α` and any other filter `g` on `α`, if the infimum (greatest lower bound) of the ultrafilter and the filter is not the bottom filter (i.e., it's not the filter containing all sets), then the ultrafilter is less than or equal to the filter `g`. In other words, all sets in the ultrafilter are also in the filter `g`.
More concisely: If an ultrafilter `f` on type `α` and filter `g` on `α` have a non-bottom infimum, then `f` is contained in `g`.
|
Ultrafilter.neBot'
theorem Ultrafilter.neBot' : ∀ {α : Type u_2} (self : Ultrafilter α), self.NeBot
This theorem states that for any type `α` and any ultrafilter `self` on that type, the ultrafilter is not trivial (or "bottom"). In mathematical terms, an ultrafilter is considered nontrivial if it does not contain every set, which is the definition of the "bottom" ultrafilter in this context. The theorem asserts this property for all ultrafilters.
More concisely: For any type `α` and ultrafilter `self` on `α`, `self` is nontrivial, i.e., not every set is in `self`.
|
Filter.exists_ultrafilter_le
theorem Filter.exists_ultrafilter_le : ∀ {α : Type u} (f : Filter α) [h : f.NeBot], ∃ u, ↑u ≤ f
This theorem, named `Filter.exists_ultrafilter_le`, describes the ultrafilter lemma. In the context of any given type `α` and a proper filter `f` of `α` (meaning the filter is not the bottom filter), it asserts that there exists an ultrafilter `u` such that `u` is a superset of `f`. In other words, any proper filter is contained in some ultrafilter.
More concisely: For any proper filter `f` on type `α`, there exists an ultrafilter `u` containing `f`.
|
Filter.iSup_ultrafilter_le_eq
theorem Filter.iSup_ultrafilter_le_eq : ∀ {α : Type u} (f : Filter α), ⨆ g, ⨆ (_ : ↑g ≤ f), ↑g = f
This theorem states that for any given filter `f` in a particular type `α`, the filter `f` is equal to the supremum (denoted by `⨆`) of all ultrafilters `g` that contain `f`. In simpler terms, it's basically saying that any filter is equivalent to the intersection of all the ultrafilters that contain it.
More concisely: Given a filter `f` on type `α`, it is equal to the supremum of all ultrafilters containing `f`. In symbols: `f = ⨆ { g : filter α | g ��supseteq f }`.
|
Ultrafilter.compl_mem_iff_not_mem
theorem Ultrafilter.compl_mem_iff_not_mem : ∀ {α : Type u} {f : Ultrafilter α} {s : Set α}, sᶜ ∈ f ↔ s ∉ f
This theorem states that for any type `α`, any ultrafilter `f` of `α`, and any set `s` of type `α`, the complement of `s` (`sᶜ`) is an element of `f` if and only if `s` is not an element of `f`. In other words, it captures the idea that in an ultrafilter, a set and its complement cannot both be present.
More concisely: For any ultrafilter `f` on type `α` and set `s` of type `α`, `s` is not in `f` if and only if its complement `sᶜ` is in `f`.
|
Set.Finite.compl_mem_hyperfilter
theorem Set.Finite.compl_mem_hyperfilter :
∀ {α : Type u} [inst : Infinite α] {s : Set α}, s.Finite → sᶜ ∈ Filter.hyperfilter α
This theorem, referred to as `Set.Finite.compl_mem_hyperfilter`, states that for any type `α` that is infinite, and for any set `s` of type `α`, if `s` is finite, then the complement of `s` (denoted as `sᶜ`) is a member of the hyperfilter of `α`. In simpler terms, for any infinite type and any finite set of that type, the set of all elements not in the original set is present in the hyperfilter of that type.
More concisely: For any infinite type `α` and finite set `s` of `α`, the complement of `s` belongs to the hyperfilter of `α`.
|
Ultrafilter.finite_sUnion_mem_iff
theorem Ultrafilter.finite_sUnion_mem_iff :
∀ {α : Type u} {f : Ultrafilter α} {s : Set (Set α)}, s.Finite → (s.sUnion ∈ f ↔ ∃ t ∈ s, t ∈ f)
This theorem states that for any type `α`, any Ultrafilter `f` on `α`, and any set `s` of subsets of `α`, if `s` is finite, then the union of all subsets in `s` belongs to the Ultrafilter `f` if and only if there exists a subset `t` in `s` such that `t` belongs to `f`. In mathematical terms, if `s` is a finite collection of subsets of `α`, the union of `s` is in `f` exactly when at least one of the subsets in `s` is in `f`.
More concisely: For any ultrafilter `f` on a type `α` and finite set `s` of subsets of `α`, the union of `s` is in `f` if and only if some subset in `s` is in `f`.
|
Ultrafilter.of_le
theorem Ultrafilter.of_le : ∀ {α : Type u} (f : Filter α) [inst : f.NeBot], ↑(Ultrafilter.of f) ≤ f
This theorem states that for any type `α` and any filter `f` on `α` that is not the bottom filter, the ultrafilter extending `f` is less than or equal to `f`. In other words, every set in the ultrafilter (obtained using the function `Ultrafilter.of`) is also a set in the original filter `f`.
More concisely: For any filter `f` on type `α` that is not the bottom filter, every set in the ultrafilter obtained from `f` using `Ultrafilter.of` is contained in `f`.
|
Filter.NeBot.le_pure_iff
theorem Filter.NeBot.le_pure_iff : ∀ {α : Type u} {f : Filter α} {a : α}, f.NeBot → (f ≤ pure a ↔ f = pure a) := by
sorry
This theorem states that for any type `α`, any filter `f` on `α`, and any element `a` of `α`, if the filter `f` is not the bottom filter, then `f` being less than or equal to the pure filter of `a` is equivalent to `f` being equal to the pure filter of `a`. In the context of filters, the "less than or equal" relation can be understood as "is a subset of". Therefore, this theorem is saying that if the filter `f` isn't the bottom filter, then if `f` is a subset of the singleton set containing only `a`, it must be the same as that singleton set.
More concisely: For any filter `f` on type `α` and element `a` of `α`, if `f` is not the bottom filter, then `f = {a}`. (Here, `{a}` denotes the pure filter of `a`.)
|
Ultrafilter.coe_inj
theorem Ultrafilter.coe_inj : ∀ {α : Type u} {f g : Ultrafilter α}, ↑f = ↑g ↔ f = g
This theorem states that for any given type `α` and ultrafilters `f` and `g` over that type, the mapping of `f` to the underlying type is equal to the mapping of `g` to the underlying type if and only if `f` is equal to `g`. In other words, two ultrafilters are equal if their mappings to the base type `α` are equal. This theorem is about the injectivity of the coe (coercion) function for ultrafilters.
More concisely: Two ultrafilters over type `α` are equal if and only if their underlying types are equal as coerced values.
|