Function.Injective.nat_tendsto_atTop
theorem Function.Injective.nat_tendsto_atTop :
∀ {f : ℕ → ℕ}, Function.Injective f → Filter.Tendsto f Filter.atTop Filter.atTop
The theorem `Function.Injective.nat_tendsto_atTop` states that for every injective sequence `f` from natural numbers to natural numbers, the limit of `f` tends to infinity when the input tends to infinity. In other words, if `f` is a function from natural numbers to natural numbers and it has the property that it always produces different outputs for different inputs (i.e., it's injective), then as the input values become larger and larger (approach infinity), the output values of `f` also become larger and larger (also approach infinity).
More concisely: If `f : ℕ → ℕ` is an injective function, then for all `x in ℕ`, the sequence `f` tends to infinity as `x` approaches infinity.
|
Function.Injective.tendsto_cofinite
theorem Function.Injective.tendsto_cofinite :
∀ {α : Type u_2} {β : Type u_3} {f : α → β},
Function.Injective f → Filter.Tendsto f Filter.cofinite Filter.cofinite
This theorem states that for an injective function `f` from a type `α` to a type `β`, the inverse image of any finite set is also finite. In other words, if `f` is such that no two different elements in `α` have the same image in `β`, then when we consider any finite set in `β` and look at its pre-images in `α` under the function `f`, the set of such pre-images is also finite. This can be thought of as a property of the function `f` "preserving" the finiteness of sets under the operation of taking pre-images. This theorem is related to the concept of "cofinite" filters, which are filters of subsets whose complements are finite.
More concisely: If `f` is an injective function from a type `α` to a type `β`, then the preimage of any finite subset of `β` under `f` is a finite subset of `α`.
|
Filter.hasBasis_cofinite
theorem Filter.hasBasis_cofinite : ∀ {α : Type u_2}, Filter.cofinite.HasBasis (fun s => s.Finite) compl
The theorem `Filter.hasBasis_cofinite` states that for all types `α`, the cofinite filter (which is the filter of subsets of `α` whose complements are finite) has a basis given by the function `Set.Finite s` applied to the complement of `s`. In other words, the cofinite filter is generated by the sets whose complements are finite.
More concisely: The cofinite filter on a type `α` is generated by the sets whose complements are finite.
|
Function.Injective.comap_cofinite_eq
theorem Function.Injective.comap_cofinite_eq :
∀ {α : Type u_2} {β : Type u_3} {f : α → β},
Function.Injective f → Filter.comap f Filter.cofinite = Filter.cofinite
This theorem states that for any types `α` and `β` and any function `f` from `α` to `β`, if `f` is injective (i.e., for all `a₁` and `a₂` in `α`, `f(a₁) = f(a₂)` implies `a₁ = a₂`), then the pullback of the cofinite filter (the filter of subsets of `β` whose complements are finite) under `f` is equivalent to the cofinite filter of `α`. In other words, pulling back the cofinite filter through an injective function doesn't change the filter. This theorem links the concepts of function injectivity and filter theory in a precise way, and is related to the theorems `Filter.comap_cofinite_le` and `Function.Injective.tendsto_cofinite`.
More concisely: For an injective function `f` from type `α` to type `β`, the pullback of the cofinite filter on `β` under `f` is equivalent to the cofinite filter on `α`.
|
Set.Infinite.frequently_cofinite
theorem Set.Infinite.frequently_cofinite :
∀ {α : Type u_2} {s : Set α}, s.Infinite → ∃ᶠ (x : α) in Filter.cofinite, x ∈ s
This theorem, referred to as `Set.Infinite.frequently_cofinite`, states that for any type `α` and any set `s` of type `α`, if `s` is infinite, then there exists a frequently occurring element `x` of type `α` in the cofinite filter such that `x` is a member of `s`. In other words, in the filter of subsets whose complements are finite, we can always find an element that shows up very often and is a member of an infinite set.
More concisely: For any infinite set `s`, there exists an element `x` in `s` that belongs to infinitely many cofinite subsets of `s`.
|
Filter.coprod_cofinite
theorem Filter.coprod_cofinite :
∀ {α : Type u_2} {β : Type u_3}, Filter.cofinite.coprod Filter.cofinite = Filter.cofinite
The theorem `Filter.coprod_cofinite` states that for any two types, `α` and `β`, the coproduct of their cofinite filters is equal to the cofinite filter on their product. In other words, when we construct the filter of all subsets whose complements are finite for each of the two types separately and then take their coproduct, it is the same as directly constructing the cofinite filter for the product of the two types.
More concisely: The coproduct of the cofinite filters on types `α` and `β` is equal to the cofinite filter on their product `α × β`.
|
Set.Infinite.cofinite_inf_principal_neBot
theorem Set.Infinite.cofinite_inf_principal_neBot :
∀ {α : Type u_2} {s : Set α}, s.Infinite → (Filter.cofinite ⊓ Filter.principal s).NeBot
This theorem states that for any type `α` and for any set `s` of type `α`, if `s` is an infinite set, then the infimum of the cofinite filter and the principal filter of `s` is not the bottom element. In other words, the intersection of the filter of all subsets of `α` whose complements are finite and the filter of all supersets of `s` does not yield the lowest possible filter (which is the empty set in this context) if `s` is an infinite set.
More concisely: For any infinite set `s` of type `α`, the infimum of the cofinite filter and the principal filter of `s` is not the empty set.
|
Mathlib.Order.Filter.Cofinite._auxLemma.1
theorem Mathlib.Order.Filter.Cofinite._auxLemma.1 : ∀ {α : Type u_2} {s : Set α}, (s ∈ Filter.cofinite) = sᶜ.Finite
This theorem from the Mathlib library in Lean states that for any type `α` and any set `s` of this type, `s` belongs to the cofinite filter if and only if the complement of `s` is a finite set. Here, the cofinite filter is defined as the collection of subsets whose complements are finite. Thus, it establishes a direct connection between the concept of cofinite filters and finite sets, specifically through the complement of a set.
More concisely: A set `s` of type `α` belongs to the cofinite filter if and only if the complement of `s` is finite.
|
Set.Finite.compl_mem_cofinite
theorem Set.Finite.compl_mem_cofinite : ∀ {α : Type u_2} {s : Set α}, s.Finite → sᶜ ∈ Filter.cofinite
This theorem states that for any type `α` and any set `s` of type `α`, if the set `s` is finite then the complement of `s` (denoted as `sᶜ`) is a member of the cofinite filter. In other words, the complement of any finite set is a subset of the universe whose complement (the original set) is finite, and thus it belongs to the cofinite filter, which is the filter of subsets with finite complements.
More concisely: For any type `α` and finite set `s` of type `α`, the complement of `s` belongs to the cofinite filter.
|
Nat.cofinite_eq_atTop
theorem Nat.cofinite_eq_atTop : Filter.cofinite = Filter.atTop
This theorem states that, in the context of natural numbers, the filters `Filter.cofinite` and `Filter.atTop` are equivalent. The filter `Filter.cofinite` represents the filter of subsets whose complements are finite, while `Filter.atTop` symbolizes the limit towards positive infinity. Thus, this theorem essentially means that the collection of subsets of natural numbers with finite complements is the same as the collection of subsets of natural numbers that contain all sufficiently large numbers.
More concisely: The filters of cofinite subsets and subsets containing all but finitely many natural numbers are equivalent.
|
Filter.Tendsto.countable_compl_preimage_ker
theorem Filter.Tendsto.countable_compl_preimage_ker :
∀ {α : Type u_2} {β : Type u_3} {f : α → β} {l : Filter β} [inst : l.IsCountablyGenerated],
Filter.Tendsto f Filter.cofinite l → (f ⁻¹' l.ker)ᶜ.Countable
This theorem states that if a function `f` from a type `α` to a type `β` tends to a countably generated filter `l` along the cofinite filter, then the set of all elements `x` in the domain of `f` for which `f(x)` is not in the kernel of `l` is countable. Here, the cofinite filter is defined as the filter of subsets whose complements are finite. In other words, if `f` has the property that the preimage of any neighborhood of `l` under `f` is a cofinite subset of the domain `α`, then there are only countably many values of `x` such that `f(x)` doesn't belong to the kernel of `l`.
More concisely: If a function from a type to another tends to a countably generated filter along the cofinite filter, then the set of elements in the domain not mapping to the filter's kernel is countable.
|
Filter.atTop_le_cofinite
theorem Filter.atTop_le_cofinite :
∀ {α : Type u_2} [inst : Preorder α] [inst_1 : NoMaxOrder α], Filter.atTop ≤ Filter.cofinite
This theorem states that if `α` is a type that has a preorder structure and there is no maximal element in `α` (formally, `α` satisfies the `NoMaxOrder` property), then the `atTop` filter on `α` is less than or equal to the `cofinite` filter on `α`. In other words, any set in `α` that is eventually always true (represented by the `atTop` filter) is also a set whose complement is finite (represented by the `cofinite` filter).
More concisely: If `α` is a preordered type without a maximal element, then the `atTop` filter is included in the `cofinite` filter.
|
Filter.countable_compl_ker
theorem Filter.countable_compl_ker :
∀ {α : Type u_2} {l : Filter α} [inst : l.IsCountablyGenerated], Filter.cofinite ≤ l → l.kerᶜ.Countable
This theorem states that for any type `α` and any filter `l` on `α` that is countably generated, if `l` is greater than or equal to the cofinite filter (i.e., the filter of subsets whose complements are finite), then the complement of `l.ker` (i.e., the set of all elements not in the kernel of `l`) is countable. In other words, it says that if a countably generated filter contains all cofinite sets, then it excludes at most countably many elements.
More concisely: If `α` is a type and `l` is a countably generated filter on `α` that contains the cofinite filter, then the complement of `l.ker` is countable.
|
Filter.frequently_cofinite_iff_infinite
theorem Filter.frequently_cofinite_iff_infinite :
∀ {α : Type u_2} {p : α → Prop}, (∃ᶠ (x : α) in Filter.cofinite, p x) ↔ {x | p x}.Infinite
This theorem states that for any type `α` and a property `p` defined for elements of `α`, the property `p` frequently holds for `x` in the cofinite filter of `α` if and only if the set of all `x` for which `p x` is true is infinite. Here, the "cofinite filter" is the collection of subsets of `α` whose complements are finite, and a set is defined as "infinite" if it is not a finite set. In other words, we can frequently find elements satisfying `p` in the cofinite filter if and only if there are infinitely many elements satisfying `p`.
More concisely: A property `p` holds frequently in the cofinite filter of a type `α` if and only if the set of elements satisfying `p` is infinite.
|
Filter.comap_cofinite_le
theorem Filter.comap_cofinite_le :
∀ {α : Type u_2} {β : Type u_3} (f : α → β), Filter.comap f Filter.cofinite ≤ Filter.cofinite
The theorem `Filter.comap_cofinite_le` states that for all types `α` and `β` and any function `f` from `α` to `β`, the cofinite filter of the preimage of `f` (which is obtained by the `Filter.comap` function) is less than or equal to the cofinite filter of `β`. In other words, the set of preimages under `f` of the cofinite subsets of `β` is a subset of the cofinite subsets of `α`.
More concisely: For all types `α` and `β` and functions `f` from `α` to `β`, the cofinite filter of `f`'s preimages is included in the cofinite filter of `β`.
|
Filter.le_cofinite_iff_eventually_ne
theorem Filter.le_cofinite_iff_eventually_ne :
∀ {α : Type u_2} {l : Filter α}, l ≤ Filter.cofinite ↔ ∀ (x : α), ∀ᶠ (y : α) in l, y ≠ x
This theorem states that for any type `α` and any filter `l` of that type, `l` is less than or equal to the cofinite filter if and only if for each element `x` of type `α`, it is eventually the case in the filter `l` that `y` is not equal to `x`. In other words, any element `x` in the filter `l` will eventually be followed by some other element `y` that is not equal to `x`.
More concisely: For any type `α` and filter `l` of `α`, `l` is equal to the cofinite filter if and only if for all `x` in `α`, there exists an `y` not equal to `x` such that `y` is in `l` and is eventually greater than `x` in `l`.
|