Filter.Tendsto.eventually
theorem Filter.Tendsto.eventually :
∀ {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop},
Filter.Tendsto f l₁ l₂ → (∀ᶠ (y : β) in l₂, p y) → ∀ᶠ (x : α) in l₁, p (f x)
The theorem `Filter.Tendsto.eventually` establishes that if a function `f` from type `α` to `β` tends to a limit and for all `y` in the limit filter `l₂`, a property `p` holds eventually, then for all `x` in the input filter `l₁`, the property `p` holds for `f(x)` eventually. In other words, this theorem asserts that if a function's output approaches a limit and in that limit a certain property is eventually true, then that property is eventually true for the function's output over its input domain.
More concisely: If a function from `α` to `β` tends to a limit and the property `p` is eventually true for all elements in the limit, then `p` is eventually true for the function's output given any input in the domain.
|
Filter.EventuallyLE.biInter
theorem Filter.EventuallyLE.biInter :
∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
s.Finite →
∀ {f g : ι → Set α}, (∀ i ∈ s, l.EventuallyLE (f i) (g i)) → l.EventuallyLE (⋂ i ∈ s, f i) (⋂ i ∈ s, g i)
This theorem, `Filter.EventuallyLE.biInter`, states that for any type `α`, any filter `l` on `α`, any type `ι`, and any finite set `s` of `ι`, if for every element `i` in `s` the filter `l` is eventually less than or equal to both the set function `f` applied to `i`, and the set function `g` applied to `i`, then the filter `l` is also eventually less than or equal to the intersection of the set `s` with the sets defined by `f` and `g` respectively. In simpler terms, if a filter is eventually less than or equal to each of a collection of sets, it is also eventually less than or equal to the intersection of those sets.
More concisely: If for all elements $i$ in a finite set $S$, filter $l$ is eventually less than or equal to both $f(i)$ and $g(i)$, then $l$ is eventually less than or equal to $f \cap g : S \to \mathit{Set} \to \mathit{Filter}(\mathit{Set})$ (the set intersection of $f$ and $g$ applied to $S$).
|
Filter.mem_top
theorem Filter.mem_top : ∀ {α : Type u} {s : Set α}, s ∈ ⊤ ↔ s = Set.univ
The theorem `Filter.mem_top` states that for any type `α` and any set `s` of type `α`, `s` is a member of the top filter if and only if `s` is the universal set of `α`. In other words, within the context of filters, the top filter only contains the universal set that includes all elements of a given type `α`.
More concisely: The top filter of a set `s` in type `α` contains exactly the universal set of `α`.
|
Filter.Frequently.and_eventually
theorem Filter.Frequently.and_eventually :
∀ {α : Type u} {p q : α → Prop} {f : Filter α},
(∃ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, q x) → ∃ᶠ (x : α) in f, p x ∧ q x
This theorem states that for any type `α`, predicates `p` and `q`, and filter `f` on `α`, if there frequently exists an `x` in `f` such that predicate `p` holds, and if it is eventually the case that for all `x` in `f`, predicate `q` holds, then there frequently exists an `x` in `f` for which both `p` and `q` hold. In other words, if a condition `p` is frequently true and another condition `q` is eventually always true in a certain context determined by a filter, then it is frequently the case that both conditions hold together.
More concisely: If a filter `f` on type `α` has infinitely many elements `x` where `p(x)` holds and eventually all elements `x` in `f` satisfy `q(x)`, then there exists an infinite subset `S` of `f` such that for all `x` in `S`, both `p(x)` and `q(x)` hold.
|
Filter.EventuallyEq.symm
theorem Filter.EventuallyEq.symm :
∀ {α : Type u} {β : Type v} {f g : α → β} {l : Filter α}, l.EventuallyEq f g → l.EventuallyEq g f
This theorem states that for any two functions `f` and `g` from type `α` to type `β` and any filter `l` on type `α`, if `f` is eventually equal to `g` at filter `l` (denoted as `f =ᶠ[l] g`), then `g` is also eventually equal to `f` at the same filter (denoted as `g =ᶠ[l] f`). In other words, the property of two functions being eventually equal at a certain filter is symmetric.
More concisely: If `f` is eventually equal to `g` at filter `l` (`f =ᶠ[l] g`), then `g` is also eventually equal to `f` at filter `l` (`g =ᶠ[l] f`). (Symmetry of eventual equality at a filter)
|
Filter.map_le_iff_le_comap
theorem Filter.map_le_iff_le_comap :
∀ {α : Type u} {β : Type v} {f : Filter α} {g : Filter β} {m : α → β}, Filter.map m f ≤ g ↔ f ≤ Filter.comap m g
This theorem states that for any types `α` and `β`, any filters `f` on `α` and `g` on `β`, and any function `m` from `α` to `β`, the filter obtained by mapping `f` through `m` is a subfilter of `g` if and only if `f` is a subfilter of the filter obtained by co-mapping `g` through `m`. In more mathematical terms, `Filter.map m f ≤ g` if and only if `f ≤ Filter.comap m g`. This provides a relationship between the operations of filter mapping and co-mapping.
More concisely: For filters $f$ on type $\alpha$ and $g$ on type $\beta$, and any function $m$ from $\alpha$ to $\beta$, the filter obtained by mapping $f$ through $m$ is a subfilter of $g$ if and only if $f$ is a subfilter of the filter obtained by co-mapping $g$ through $m$.
|
Filter.NeBot.ne'
theorem Filter.NeBot.ne' : ∀ {α : Type u} {f : Filter α} [self : f.NeBot], f ≠ ⊥
This theorem states that for any type `α` and any filter `f` on `α`, if `f` is nontrivial (that is, it has the property `f.NeBot`), then `f` is not the bottom filter. In the language of set theory, this means that the empty set is not an element of `f`.
More concisely: If `f` is a nontrivial filter on type `α` in Lean 4, then `∅ ∉ f`.
|
Filter.tendsto_map
theorem Filter.tendsto_map :
∀ {α : Type u} {β : Type v} {f : α → β} {x : Filter α}, Filter.Tendsto f x (Filter.map f x)
This theorem `Filter.tendsto_map` asserts that for any function `f` from type `α` to `β` and any filter `x` on `α`, the function `f` tends to the map of the filter `x` under `f`. In other words, for every neighborhood of `f`-images (or set of `f`-images) in the `f`-mapped filter `x`, the preimage under `f` of this set is a neighborhood in the original filter `x`. This is a universal property of functions and filters, essentially stating that the function `f` respects the filter structure.
More concisely: For any filter `x` on `α` and function `f` from `α` to `β`, if for every neighborhood `V` of `f(x)` in `β`, `f⁁¹(V)` is a neighborhood of `x` in `α`, then `x` tends to the map `f(x)` under `f`.
|
Filter.EventuallyEq.sub
theorem Filter.EventuallyEq.sub :
∀ {α : Type u} {β : Type v} [inst : Sub β] {f f' g g' : α → β} {l : Filter α},
l.EventuallyEq f g → l.EventuallyEq f' g' → l.EventuallyEq (fun x => f x - f' x) fun x => g x - g' x
This theorem is stating that for any types `α` and `β`, given a Subtraction instance for `β`, and functions `f`, `f'`, `g`, and `g'` from `α` to `β`, along with a filter `l` on `α`, if `f` eventually equals `g` at the filter `l` and `f'` eventually equals `g'` at the same filter, then the function that subtracts `f'` from `f` will eventually equal the function that subtracts `g'` from `g` at that filter. In shorthand, if `f ≈ g` and `f' ≈ g'` at some point according to a filter, then `(f - f') ≈ (g - g')` according to the same filter.
More concisely: For types `α` and `β` with Subtraction instances, if functions `f, f', g, g' : α → β` satisfy `f ≈ g` and `f' ≈ g'` at some filter `l` on `α`, then `(f - f') ≈ (g - g')` at filter `l`.
|
Filter.disjoint_comap_iff
theorem Filter.disjoint_comap_iff :
∀ {α : Type u} {β : Type v} {g₁ g₂ : Filter β} {m : α → β},
Function.Surjective m → (Disjoint (Filter.comap m g₁) (Filter.comap m g₂) ↔ Disjoint g₁ g₂)
The theorem `Filter.disjoint_comap_iff` states that for any types `α` and `β`, filters `g₁` and `g₂` on `β`, and a surjective function `m` from `α` to `β`, the preimage filters of `g₁` and `g₂` under `m` are disjoint if and only if `g₁` and `g₂` themselves are disjoint. Here, two elements of a lattice (in this case, the lattice of filters) are said to be disjoint if their infimum is the bottom element. A function is surjective if every element of the codomain is the image of some element of the domain under the function.
More concisely: For filters $g\_1$ and $g\_2$ on type $\beta$, and a surjective function $m$ from type $\alpha$ to $\beta$, the preimages of $g\_1$ and $g\_2$ under $m$ are disjoint if and only if $g\_1$ and $g\_2$ themselves are disjoint in the lattice of filters.
|
Filter.mem_principal_self
theorem Filter.mem_principal_self : ∀ {α : Type u} (s : Set α), s ∈ Filter.principal s
The theorem `Filter.mem_principal_self` states that for any type `α` and any set `s` of type `α`, the set `s` is a member of its own principal filter. In other words, considering the principal filter as a collection of all supersets of `s`, `s` is always a superset of itself, and therefore belongs to its own principal filter.
More concisely: For any set `s` of type `α`, `s` is a subset of its principal filter.
|
Filter.tendsto_principal
theorem Filter.tendsto_principal :
∀ {α : Type u} {β : Type v} {f : α → β} {l : Filter α} {s : Set β},
Filter.Tendsto f l (Filter.principal s) ↔ ∀ᶠ (a : α) in l, f a ∈ s
This theorem, `Filter.tendsto_principal`, states that for any given types `α` and `β`, a function `f` from `α` to `β`, a filter `l` on `α`, and a set `s` of `β`, the function `f` tends to the principal filter of `s` (meaning that the image of `f` gets arbitrarily close to `s` as defined by the filter `l`) if and only if for almost all `a` in `l`, the image `f(a)` is an element of `s`. In other words, it relates the concept of a function tending towards a filter to the idea of almost all elements of a filter being mapped into a certain set by a function.
More concisely: A function from a type to another tends to the principal filter of a set if and only if the image of almost all elements in the filter is contained in the set.
|
Filter.Frequently.mono
theorem Filter.Frequently.mono :
∀ {α : Type u} {p q : α → Prop} {f : Filter α},
(∃ᶠ (x : α) in f, p x) → (∀ (x : α), p x → q x) → ∃ᶠ (x : α) in f, q x
This theorem states that if there exists a filter `f` in a type `α` such that a predicate `p` holds frequently within `f`, and if for all `x` of type `α` `p x` implies `q x`, then `q x` also holds frequently within the filter `f`. In other words, the theorem asserts the preservation of frequency under a filter for a property when that property implies another one.
More concisely: If a filter `f` in type `α` has property `p` holding frequently and `p(x)` implies `q(x)` for all `x` in `α`, then property `q` holds frequently within filter `f`.
|
Filter.tendsto_pure_pure
theorem Filter.tendsto_pure_pure :
∀ {α : Type u} {β : Type v} (f : α → β) (a : α), Filter.Tendsto f (pure a) (pure (f a))
The theorem `Filter.tendsto_pure_pure` asserts that for any function `f` from type `α` to type `β` and any element `a` of type `α`, the function `f` tends to the filter `pure (f a)` when applied to the filter `pure a`. In other words, for every neighborhood of `f a`, the preimage under `f` of this neighborhood contains `a`, which is the essence of the definition of 'tending to' in the context of filters.
More concisely: For any function `f: α → β` and `a ∈ α`, the filter `{x : α | ∃ ε > 0, ∀ x' ∈ β, 0 < d(x, f x') < ε ⇒ x ∈ filter.pure a}` tends to `f a`.
|
Filter.not_neBot
theorem Filter.not_neBot : ∀ {α : Type u} {f : Filter α}, ¬f.NeBot ↔ f = ⊥
This theorem states that for every given type `α` and a filter `f` of that type, the filter `f` is not 'neBot' if and only if `f` is the bottom filter (notated as `⊥`). In other words, a filter `f` is not 'neBot' (not apart from the bottom filter) precisely when `f` itself is the bottom filter. This is a characteristic property of the bottom filter in the filter theory.
More concisely: A filter is not the negation of the bottom filter if and only if it is the bottom filter itself.
|
Filter.EventuallyEq.prod_mk
theorem Filter.EventuallyEq.prod_mk :
∀ {α : Type u} {β : Type v} {γ : Type w} {l : Filter α} {f f' : α → β},
l.EventuallyEq f f' →
∀ {g g' : α → γ}, l.EventuallyEq g g' → l.EventuallyEq (fun x => (f x, g x)) fun x => (f' x, g' x)
This theorem states that for any types `α`, `β`, and `γ`, and any filter `l` on `α`, if two functions `f` and `f'` from `α` to `β` are eventually equal with respect to the filter `l`, and two other functions `g` and `g'` from `α` to `γ` are also eventually equal with respect to the same filter, then the function that maps `x` in `α` to the pair `(f x, g x)` is eventually equal to the function mapping `x` to `(f' x, g' x)` with respect to the filter `l`. In other words, if the components of two functions from `α` to the product type `(β, γ)` are each eventually equal, then the two functions themselves are eventually equal.
More concisely: If functions `f` and `f'` from `α` to `β`, and functions `g` and `g'` from `α` to `γ`, are each eventually equal with respect to filter `l`, then the functions `(λ x, (f x, g x))` and `(λ x, (f' x, g' x))` from `α` to `(β × γ)` are eventually equal with respect to `l`.
|
Filter.mem_iInf_of_iInter
theorem Filter.mem_iInf_of_iInter :
∀ {α : Type u} {ι : Type u_2} {s : ι → Filter α} {U : Set α} {I : Set ι},
I.Finite → ∀ {V : ↑I → Set α}, (∀ (i : ↑I), V i ∈ s ↑i) → ⋂ i, V i ⊆ U → U ∈ ⨅ i, s i
The theorem `Filter.mem_iInf_of_iInter` states that for any two types `α` and `ι`, a function from `ι` to `Filter α`, a set `U` of type `α`, and a finite set `I` of type `ι`, if for each element `i` in `I`, the set `V i` is an element of the filter corresponding to `i`, and the intersection of all the sets `V i` is a subset of `U`, then `U` is an element of the infimum of the filters corresponding to each `i` in `I`. In simpler words, if every set in a collection is in the corresponding filter, and their intersection is contained in a set, then that set is in the intersection of the filters.
More concisely: If for each `i` in a finite set `I`, `V i` is an element of the filter `F i` on `α`, and `∩_{i ∈ I} V i ⊆ U`, then `U` is an element of `∏_{i ∈ I} F i`. (Here, `∏_{i ∈ I} F i` denotes the infimum or meet of the filters `F i`.)
|
Filter.disjoint_of_disjoint_of_mem
theorem Filter.disjoint_of_disjoint_of_mem :
∀ {α : Type u} {f g : Filter α} {s t : Set α}, Disjoint s t → s ∈ f → t ∈ g → Disjoint f g
This theorem states that for any type `α`, any two filters `f` and `g` on this type, and any two sets `s` and `t` of this type, if `s` and `t` are disjoint and `s` belongs to filter `f` and `t` belongs to filter `g`, then filters `f` and `g` are also disjoint. Here, two sets are said to be disjoint if they have no elements in common, and two filters are considered disjoint if their infimum (or greatest lower bound) is the bottom element of the lattice structure.
More concisely: Given filters `f` and `g` on type `α`, if sets `s` in `f` and `t` in `g` are disjoint, then filters `f` and `g` are disjoint in the sense that their infimum is the bottom element of the lattice structure.
|
Filter.univ_mem'
theorem Filter.univ_mem' : ∀ {α : Type u} {f : Filter α} {s : Set α}, (∀ (a : α), a ∈ s) → s ∈ f
This theorem, named `Filter.univ_mem'`, states that for any type `α`, any filter `f` on `α`, and any set `s` of type `α`, if every element `a` of type `α` belongs to the set `s`, then the set `s` is a member of the filter `f`. In other words, it states that if all elements of a particular type are in a set, that set is part of a certain filter.
More concisely: If `s` is a set of type `α` and every element `a` of `α` belongs to `s`, then `s` is an element of filter `f` on type `α`.
|
Filter.map_congr
theorem Filter.map_congr :
∀ {α : Type u} {β : Type v} {m₁ m₂ : α → β} {f : Filter α},
f.EventuallyEq m₁ m₂ → Filter.map m₁ f = Filter.map m₂ f
The theorem `Filter.map_congr` states that for any types `α` and `β`, any two functions `m₁` and `m₂` from `α` to `β`, and any filter `f` on `α`, if `m₁` and `m₂` are eventually equal at the filter `f` (denoted by `m₁ =ᶠ[f] m₂`), then the forward maps of the filter `f` under `m₁` and `m₂`, denoted by `Filter.map m₁ f` and `Filter.map m₂ f` respectively, are equal. In simpler terms, if two functions agree on the elements of a set that are close enough to a particular value, then the filters obtained by applying these functions to the original filter are the same.
More concisely: If two functions agree at the filter convergence, then their filter maps are equal.
|
Mathlib.Order.Filter.Basic._auxLemma.65
theorem Mathlib.Order.Filter.Basic._auxLemma.65 : ∀ {a b : Prop}, (a → b) = (¬a ∨ b)
This theorem, named `Mathlib.Order.Filter.Basic._auxLemma.65`, states that for any two propositions `a` and `b`, the implication from `a` to `b` is equivalent to the disjunction of the negation of `a` or `b`. In other words, the statement "if `a` then `b`" is logically equivalent to the statement "either `a` is not true, or `b` is true".
More concisely: The implication `a → b` is logically equivalent to the disjunction `¬a ∨ b`.
|
Filter.le_pure_iff
theorem Filter.le_pure_iff : ∀ {α : Type u} {f : Filter α} {a : α}, f ≤ pure a ↔ {a} ∈ f
This theorem, `Filter.le_pure_iff`, states that for any type `α`, any filter `f` of type `α`, and any element `a` of type `α`, the filter `f` is less than or equal to the pure filter of `a` if and only if the singleton set containing `a` is in the filter `f`. In other words, a filter `f` includes the pure filter of `a` when the set containing only `a` is an element of the filter `f`.
More concisely: A filter `f` of type `α` includes the pure filter of `a` if and only if `{a} ∈ f`.
|
Filter.map_mono
theorem Filter.map_mono : ∀ {α : Type u} {β : Type v} {m : α → β}, Monotone (Filter.map m)
The theorem `Filter.map_mono` states that for all types `α` and `β`, and for any function `m` from `α` to `β`, the map of a filter under the function `m` is monotone. This means that if `f` and `g` are filters on `α` and `f ≤ g`, then the filter resulting from mapping `f` through `m` is less than or equal to the filter resulting from mapping `g` through `m`, where the order on filters is defined by inclusion of their sets.
More concisely: For all types `α` and `β` and functions `m` from `α` to `β`, if `f` and `g` are filters on `α` with `f ⊆ g`, then `m(f) ⊆ m(g)`.
|
Filter.tendsto_inf
theorem Filter.tendsto_inf :
∀ {α : Type u} {β : Type v} {f : α → β} {x : Filter α} {y₁ y₂ : Filter β},
Filter.Tendsto f x (y₁ ⊓ y₂) ↔ Filter.Tendsto f x y₁ ∧ Filter.Tendsto f x y₂
The `Filter.tendsto_inf` theorem states that for any given function `f` from some type `α` to some type `β`, and any filter `x` on `α` and filters `y₁` and `y₂` on `β`, the function `f` has a limit at the intersection of `y₁` and `y₂` if and only if `f` has a limit at both `y₁` and `y₂`. In other words, the limit of `f` evaluated at `x` exists in the intersection of the filters `y₁` and `y₂` when the limit of `f` evaluated at `x` exists in both `y₁` and `y₂` separately.
More concisely: The theorem asserts that a function's limit at the intersection of two filters exists if and only if it exists in each filter separately.
|
Filter.filter_eq
theorem Filter.filter_eq : ∀ {α : Type u} {f g : Filter α}, f.sets = g.sets → f = g
This theorem states that for any two filters `f` and `g` of the same type `α`, if their sets of elements are equal, then the filters themselves are equal. In other words, two filters are identical if and only if they contain the same sets.
More concisely: If two filters `f` and `g` over type `α` have equal elements, then `f = g`.
|
Filter.Tendsto.congr
theorem Filter.Tendsto.congr :
∀ {α : Type u} {β : Type v} {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β},
(∀ (x : α), f₁ x = f₂ x) → Filter.Tendsto f₁ l₁ l₂ → Filter.Tendsto f₂ l₁ l₂
The theorem `Filter.Tendsto.congr` states that for any two functions `f₁` and `f₂` from a type `α` to a type `β`, and any two filters `l₁` over `α` and `l₂` over `β`, if every output of `f₁` equals the output of `f₂` for all inputs, then if `f₁` tends to the limit `l₂` under the filter `l₁`, `f₂` also tends to the same limit under the same filter. In other words, this theorem asserts that if two functions are equivalent, their limits at a point, if exist, are also equivalent.
More concisely: If functions `f₁` and `f₂` map the same output for all inputs in filters `l₁` over `α` and `l₂` over `β`, then `f₁` tends to the limit `l₂` if and only if `f₂` tends to the same limit under `l₁`.
|
Filter.filter_eq_bot_of_isEmpty
theorem Filter.filter_eq_bot_of_isEmpty : ∀ {α : Type u} [inst : IsEmpty α] (f : Filter α), f = ⊥
This theorem states that for any type `α` which is empty (i.e., there are no values of this type), any filter `f` over this type `α` is equal to the bottom filter. The bottom filter, denoted by `⊥`, is the smallest filter which is included in all other filters. Basically, if there are no elements in the type, any filter on that type can only be the empty filter.
More concisely: For any empty type `α`, the bottom filter `⊥` is the unique filter over `α`.
|
Filter.eventually_of_forall
theorem Filter.eventually_of_forall :
∀ {α : Type u} {p : α → Prop} {f : Filter α}, (∀ (x : α), p x) → ∀ᶠ (x : α) in f, p x
This theorem, `Filter.eventually_of_forall`, states that for any type `α`, any predicate `p` of type `α → Prop`, and any filter `f` of type `Filter α`, if `p` is true for all `x` of type `α`, then `p` is eventually true for `x` under the filter `f`. In other words, if a statement holds for all elements in a set, it will hold for elements 'eventually' in any filter applied to that set.
More concisely: For any type `α`, filter `f` of type `Filter α`, and predicate `p` of type `α → Prop`, if `p` holds for all elements in the underlying set, then there exists a finite subset whose elements have `p` holding under the filter `f`.
|
Filter.Frequently.exists
theorem Filter.Frequently.exists : ∀ {α : Type u} {p : α → Prop} {f : Filter α}, (∃ᶠ (x : α) in f, p x) → ∃ x, p x := by
sorry
This theorem states that for any type `α`, any property `p` of `α`, and any filter `f` on `α`, if there frequently exists (`∃ᶠ`) an `x` in the filter `f` such that the property `p` holds, then there exists at least one `x` for which the property `p` holds. In essense, this theorem connects the concept of "frequently" in the context of filters with the ordinary existence of an element satisfying a property.
More concisely: If a filter on a type contains an element satisfying a property "frequently," then it contains at least one element satisfying that property.
|
Filter.map_principal
theorem Filter.map_principal :
∀ {α : Type u} {β : Type v} {s : Set α} {f : α → β},
Filter.map f (Filter.principal s) = Filter.principal (f '' s)
The theorem `Filter.map_principal` states that for every type `α` and `β`, for every set `s` of type `α`, and for every function `f` that maps from `α` to `β`, mapping `f` over the principal filter of `s` results in the principal filter of the image of `s` under `f`. In other words, if we first form the collection of all supersets of `s` (principal filter of `s`), and then apply the function `f` to all elements in this collection, we get the same result as if we first applied `f` to each element in `s` and then formed the collection of all supersets of the resulting set. This emphasizes the preserving nature of the function `f` and the consistency of filter operations across different types.
More concisely: For any type `α`, set `s` of type `α`, and function `f` from `α` to `β`, the image of the principal filter of `s` under `f` is equal to the principal filter of the image of `s` under `f`.
|
Filter.tendsto_comap_iff
theorem Filter.tendsto_comap_iff :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {a : Filter α} {c : Filter γ},
Filter.Tendsto f a (Filter.comap g c) ↔ Filter.Tendsto (g ∘ f) a c
The theorem `Filter.tendsto_comap_iff` establishes an equivalence between two conditions regarding function limits for given types `α`, `β`, and `γ`, and for functions `f : α → β` and `g : β → γ`, and filters `a : Filter α` and `c : Filter γ`. The first condition states that the function `f` tends to the filter obtained by the preimage (comap) of `g` over `c` starting from `a`. The second condition states that the composition function `(g ∘ f)` tends to the filter `c` starting from `a`. In other words, the limit of `f` at the preimage of `g` over `c` is equivalent to the limit of `g ∘ f` at `c`.
More concisely: The theorem `Filter.tendsto_comap_iff` states that a function `f : α → β` tends to the filter obtained by the preimage (composition with `g : β → γ`) of a filter `c : Filter γ` over `f`'s image of a filter `a : Filter α`, if and only if the composition `g ∘ f` tends to `c` over `a`.
|
Filter.NeBot.nonempty_of_mem
theorem Filter.NeBot.nonempty_of_mem : ∀ {α : Type u} {f : Filter α}, f.NeBot → ∀ {s : Set α}, s ∈ f → s.Nonempty := by
sorry
The theorem `Filter.NeBot.nonempty_of_mem` states that for any type `α` and any filter `f` on `α` that is not a bottom filter (denoted by `Filter.NeBot f`), if a set `s` of `α` is in the filter `f` (denoted by `s ∈ f`), then the set `s` is not empty. In other words, if a set is a member of a non-bottom filter, it cannot be an empty set.
More concisely: For any filter `f` on a type `α` that is not a bottom filter (`Filter.NeBot f`), if `s ∈ f`, then `s` is a non-empty set.
|
Mathlib.Order.Filter.Basic._auxLemma.25
theorem Mathlib.Order.Filter.Basic._auxLemma.25 : ∀ {α : Type u} {s : Set α}, (s ∈ ⊥) = True
This theorem states that for any type `α` and any set `s` of elements of type `α`, it is always true that `s` is an element of the bottom filter, denoted by `⊥`. A filter is a mathematical concept that generalizes the notion of a subsequence in sequences and the notion of an "open neighborhood" in topology. The bottom filter, `⊥`, is the smallest filter that contains all subsets of the type `α`.
More concisely: For any type `α` and set `s` of elements from `α`, `s` is an element of the bottom filter `⊥`.
|
Filter.tendsto_inf_left
theorem Filter.tendsto_inf_left :
∀ {α : Type u} {β : Type v} {f : α → β} {x₁ x₂ : Filter α} {y : Filter β},
Filter.Tendsto f x₁ y → Filter.Tendsto f (x₁ ⊓ x₂) y
The theorem `Filter.tendsto_inf_left` states that for all types `α` and `β`, and for any function `f` from `α` to `β`, and any filters `x₁`, `x₂` on `α` and `y` on `β`, if the function `f` tends to filter `y` along `x₁`, then `f` also tends to `y` along the infimum (greatest lower bound) of `x₁` and `x₂`. In other words, if `f` maps every neighborhood of `x₁` to a neighborhood in `y`, it will also map every neighborhood of `x₁` intersected with `x₂` to a neighborhood in `y`.
More concisely: If a function tends to a filter at a point, it also tends to the infimum of two filters at that point.
|
Filter.comap_top
theorem Filter.comap_top : ∀ {α : Type u} {β : Type v} {m : α → β}, Filter.comap m ⊤ = ⊤
This theorem states that for any types `α` and `β`, and any function `m` from `α` to `β`, the preimage (or inverse image) filter of the function `m` at the top filter in the codomain `β` is always the top filter. In mathematical terms, given a function `m: α → β`, the filter `Filter.comap m ⊤` is equal to `⊤`. Simply put, mapping anything under the function `m` from the most general filter (top filter) will result in the most general filter.
More concisely: For any function `m: α → β`, the preimage filter of the top filter through `m` equals the top filter in the lattice of filters over `β`.
|
Filter.map_comap_of_mem
theorem Filter.map_comap_of_mem :
∀ {α : Type u} {β : Type v} {f : Filter β} {m : α → β}, Set.range m ∈ f → Filter.map m (Filter.comap m f) = f := by
sorry
The theorem `Filter.map_comap_of_mem` states that for any types `α` and `β`, any filter `f` on `β`, and any function `m` from `α` to `β`, if the range of the function `m` is a member of the filter `f`, then mapping the function `m` over the comap of `m` and `f` is equal to the original filter `f`. In other words, this theorem shows a kind of 'undoing' property of the mapping and comapping operations: if the range of the mapping function is in the filter, then comapping and mapping in sequence effectively recovers the original filter.
More concisely: For any filter `f` on type `β`, function `m` from `α` to `β`, and element `x` of `β` such that `m(x) ∈ f`, we have `m '' f = f`.
|
Filter.EventuallyEq.mul
theorem Filter.EventuallyEq.mul :
∀ {α : Type u} {β : Type v} [inst : Mul β] {f f' g g' : α → β} {l : Filter α},
l.EventuallyEq f g → l.EventuallyEq f' g' → l.EventuallyEq (fun x => f x * f' x) fun x => g x * g' x
This theorem states that for any types `α` and `β`, where `β` is a multiplicative structure, given any four functions `f`, `f'`, `g`, and `g'` from `α` to `β` and a filter `l` on `α`, if `f` is eventually equal to `g` at filter `l` and `f'` is eventually equal to `g'` at the same filter `l`, then the function that takes `x` to `f(x) * f'(x)` is eventually equal to the function that takes `x` to `g(x) * g'(x)` at filter `l`. In other words, eventual equality of functions respects multiplication under a filter.
More concisely: For any types `α` and `β` (where `β` is a multiplicative structure), given functions `f, f', g, g': α -> β`, and a filter `l` on `α`, if `f` is eventually equal to `g` at `l` and `f'` is eventually equal to `g'` at `l`, then `x ∈ l` implies `f(x) * f'(x) = g(x) * g'(x)`.
|
Filter.Tendsto.not_tendsto
theorem Filter.Tendsto.not_tendsto :
∀ {α : Type u} {β : Type v} {f : α → β} {a : Filter α} {b₁ b₂ : Filter β},
Filter.Tendsto f a b₁ → ∀ [inst : a.NeBot], Disjoint b₁ b₂ → ¬Filter.Tendsto f a b₂
The theorem `Filter.Tendsto.not_tendsto` states that given arbitrary types `α` and `β`, a function `f` from `α` to `β`, a filter `a` on `α`, and two filters `b₁` and `b₂` on `β`, if `f` tends to `b₁` along `a` and `a` is not the trivial filter, then if `b₁` and `b₂` are disjoint filters, `f` cannot tend to `b₂` along `a`. In other words, a function cannot approach two disjoint filters simultaneously along a non-trivial filter.
More concisely: If a function from a non-trivial filter on one set to disjoint filters on another set tends to one of those filters, it cannot tend to the other filter along the same filter.
|
Filter.gc_map_comap
theorem Filter.gc_map_comap :
∀ {α : Type u} {β : Type v} (m : α → β), GaloisConnection (Filter.map m) (Filter.comap m)
The theorem `Filter.gc_map_comap` states that for any type `α` and `β`, and any function `m` mapping from `α` to `β`, there is a Galois Connection between the function `Filter.map m`, which transforms a filter on `α` into a filter on `β` by applying `m`, and the function `Filter.comap m`, which computes the preimage of a filter on `β` under `m` to give a filter on `α`. In other words, for all filters `a` on `α` and `b` on `β`, the filter obtained by mapping `a` through `m` is less than or equal to `b` if and only if `a` is less than or equal to the filter obtained by taking the preimage of `b` under `m`. This theorem relates the concept of Galois Connections to the operations of mapping and taking preimages of filters.
More concisely: For any function `m` between types `α` and `β`, the maps `Filter.map m` and `Filter.comap m` define a Galois connection between filters on `α` and `β`, meaning that `Filter.map m (Filter.downset x a) = Filter.downset (m x) (Filter.map m a)` and `Filter.map m (Filter.upset x a) = Filter.upset (m x) (Filter.comap m a)` for all `x` in `α` and filters `a` on `α`.
|
Filter.EventuallyLE.antisymm
theorem Filter.EventuallyLE.antisymm :
∀ {α : Type u} {β : Type v} [inst : PartialOrder β] {l : Filter α} {f g : α → β},
l.EventuallyLE f g → l.EventuallyLE g f → l.EventuallyEq f g
This theorem is stating that for any types `α` and `β`, where `β` is a partially ordered set, and any filter `l` on `α`, and any two functions `f` and `g` from `α` to `β`, if `f` is less than or equal to `g` almost everywhere with respect to the filter `l`, and `g` is also less than or equal to `f` almost everywhere with respect to the same filter, then `f` and `g` are equal almost everywhere with respect to that filter. In more mathematical terms, this theorem states that if $f \leq g$ and $g \leq f$ almost everywhere on a set `α` with respect to a filter `l`, then $f = g$ almost everywhere on that set with respect to the same filter.
More concisely: If functions $f$ and $g$ from a set $\alpha$ to a partially ordered set $\beta$ satisfy $f \leq g$ and $g \leq f$ almost everywhere with respect to a filter $l$ on $\alpha$, then $f = g$ almost everywhere with respect to $l$.
|
Filter.sup_principal
theorem Filter.sup_principal :
∀ {α : Type u} {s t : Set α}, Filter.principal s ⊔ Filter.principal t = Filter.principal (s ∪ t)
The theorem `Filter.sup_principal` states that for any type `α` and any two sets `s` and `t` of this type, the supremum (or join) of the principal filters of `s` and `t` is equal to the principal filter of the union of `s` and `t`. In other words, the collection of all supersets of either `s` or `t` is the same as the collection of all supersets of the union of `s` and `t`.
More concisely: The principal filters of sets `s` and `t` have the same supremum as the principal filter of their union in type `α`.
|
Filter.sets_of_superset
theorem Filter.sets_of_superset :
∀ {α : Type u_1} (self : Filter α) {x y : Set α}, x ∈ self.sets → x ⊆ y → y ∈ self.sets
This theorem states that for any type `α` and a filter on this type (`self`), if a set `x` is within the sets of the filter and `x` is a subset of another set `y`, then `y` is also within the sets of the filter. In other words, if a set belongs to a filter, any superset of that set also belongs to the filter.
More concisely: If `α` is a type, `self` is a filter on `α`, and `x` is a set within `self` such that `x` is a subset of `y`, then `y` is also within `self`.
|
Filter.EventuallyEq.preimage
theorem Filter.EventuallyEq.preimage :
∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β},
l.EventuallyEq f g → ∀ (s : Set β), l.EventuallyEq (f ⁻¹' s) (g ⁻¹' s)
The theorem `Filter.EventuallyEq.preimage` states that for any types `α` and `β`, any filter `l` on `α`, and any two functions `f` and `g` from `α` to `β`, if `f` and `g` are eventually equal at filter `l`, then for any set `s` of `β`, the preimages of `s` under `f` and `g` are also eventually equal at filter `l`. In plain terms, if two functions become identical beyond a certain point (as determined by the filter), then their preimages (the set of inputs that map to a particular set of outputs) will also become identical beyond that point.
More concisely: If functions `f` and `g` are eventually equal at filter `l` on type `α`, then their preimages of any set `s` in `β` are eventually equal at filter `l`.
|
Filter.eventually_map
theorem Filter.eventually_map :
∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {P : β → Prop},
(∀ᶠ (b : β) in Filter.map m f, P b) ↔ ∀ᶠ (a : α) in f, P (m a)
This theorem establishes an equivalence between two forms of expressing a property that holds "eventually" in the context of a filter. Specifically, given a filter `f` over a type `α`, a mapping function `m` from `α` to `β`, and a property `P` over `β`, the property `P` holds eventually for all `b` in the filter obtained by mapping `f` through `m` if and only if the property `P` applied to `m a` holds eventually for all `a` in the filter `f`.
More concisely: Given a filter `f` over type `α`, a mapping function `m : α → β`, and a property `P : β → Prop`, the filter `f` maps `P` eventually if and only if the image filter `{ m(a) | a ∈ f }` has `P` as an eventual property.
|
Filter.tendsto_id
theorem Filter.tendsto_id : ∀ {α : Type u} {x : Filter α}, Filter.Tendsto id x x
The theorem `Filter.tendsto_id` states that for any given type `α` and for any filter `x` of this type, the identity function, denoted by `id`, has the property of `Filter.Tendsto`. In other words, the identity function preserves the filter structure, meaning that for every neighborhood of `x` (in the target space), the pre-image under the identity function is also a neighborhood of `x` (in the source space). This makes the identity function continuous in the filter-based topology.
More concisely: For any filter `x` on type `α`, the identity function `id : α → α` is continuous from the filter-based topology perspective, that is, for every neighborhood `v` of a point `x` in the target space, the preimage `id⁻¹[v]` is a neighborhood of `x` in the source space.
|
Filter.map_map
theorem Filter.map_map :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : Filter α} {m : α → β} {m' : β → γ},
Filter.map m' (Filter.map m f) = Filter.map (m' ∘ m) f
The theorem `Filter.map_map` states that for any types `α`, `β`, and `γ`, and for any filter `f` on `α` and any functions `m : α → β` and `m' : β → γ`, applying the function `m'` to the filter resulting from applying `m` to `f` is the same as applying the function `m' ∘ m` to the filter `f`. This is essentially a statement of function composition in the context of filter maps, and captures the intuition that the order of applying filter maps doesn't matter if we adjust the functions accordingly.
More concisely: Given filters `f` on type `α`, functions `m : α → β` and `m' : β → γ`, the application of `m'` to the filter obtained by applying `m` to `f` is equivalent to the application of `m' ∘ m` to `f`.
|
Filter.biInter_finset_mem
theorem Filter.biInter_finset_mem :
∀ {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} (is : Finset β), ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
This theorem, `Filter.biInter_finset_mem`, states that for any given filter `f` of type `α`, and a function `s` mapping from type `β` to a set of type `α`, and also a finite set `is` of type `β`, the intersection over all elements `i` in `is` of `s i` belongs to the filter `f` if and only if each individual `s i` for all `i` in `is` belongs to the filter `f`. In mathematical terms, this means that the intersection over a finite set of sets, each belonging to a filter, belongs to the filter itself.
More concisely: For any filter `f` on type `α`, and a function `s` from type `β` to `α`, if `s i ∈ f` for all `i` in a finite set `is` of type `β`, then `∩ i in is (s i) ∈ f`.
|
Filter.comap_id
theorem Filter.comap_id : ∀ {α : Type u} {f : Filter α}, Filter.comap id f = f
This theorem states that for all types `α` and for all filters `f` of type `α`, the comap (comap stands for the preimage or the inverse image function) of the identity function `id` on the filter `f` is equal to `f` itself. In terms of mathematical language, given a filter `f` on a set `α`, the preimage of `f` under the identity mapping is just `f`. This is a property of filters in the context of topology or set theory.
More concisely: For all filters $f$ on a type $\alpha$, the preimage of $f$ under the identity function is equal to $f$ (i.e., comap(id) $f$ = $f$).
|
Filter.le_comap_map
theorem Filter.le_comap_map :
∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β}, f ≤ Filter.comap m (Filter.map m f)
The theorem `Filter.le_comap_map` states that for any types `α` and `β`, for any filter `f` on `α`, and for any function `m` from `α` to `β`, the filter `f` is a subset of the filter obtained by taking the comap of the function `m` and the map of the function `m` over the filter `f`. This means that every set in the filter `f` is also in the filter formed by mapping `m` over `f` and then taking the comap of `m`.
More concisely: For any filter $f$ on type $\alpha$ and function $m:\alpha \to \beta$, we have $f \subseteq \text{comap}(m) \circ \text{map}(m)(f)$.
|
Mathlib.Order.Filter.Basic._auxLemma.131
theorem Mathlib.Order.Filter.Basic._auxLemma.131 :
∀ {α : Type u} {β : Type v} {m : α → β} {f : Filter α} {s : Set β},
(s ∈ Filter.kernMap m f) = ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ
This theorem states that for all types `α` and `β`, a mapping `m` from `α` to `β`, a filter `f` on `α`, and a set `s` of `β` elements, whether `s` is in the kernel map of `m` and `f` is equivalent to the existence of a set `t` such that the complement of `t` is in `f` and the image of `t` under `m` is equal to the complement of `s`. In other words, `s` belongs to the kernel map of `m` and `f` if and only if there is a set `t` with these properties regarding `f` and `m`.
More concisely: For any filter $f$ on type $\alpha$, set $s$ in type $\beta$, and mapping $m$ from $\alpha$ to $\beta$, $s$ is in the kernel of $m$ with respect to $f$ if and only if there exists a set $t$ such that $t$ is disjoint from $f$ and $m(t) = \complement s$.
|
Filter.mem_iInf_of_mem
theorem Filter.mem_iInf_of_mem :
∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} (i : ι) {s : Set α}, s ∈ f i → s ∈ ⨅ i, f i
The theorem `Filter.mem_iInf_of_mem` states that for any type `α` and an index type `ι`, given a function `f` from `ι` to the type of filters on `α`, an index `i` of type `ι`, and a set `s` of type `α`, if the set `s` is an element of the filter `f(i)`, then `s` is also an element of the infimum (⨅ i) of all the filters generated by `f` across all indices. In simpler terms, it states that if a set belongs to a particular filter, then it also belongs to the intersection of all filters generated by the function `f`.
More concisely: If `s` is an element of `f(i)` for some index `i` and function `f` mapping indices to filters on `α`, then `s` is an element of the infimum of all filters in the image of `f`.
|
Filter.EventuallyLE.refl
theorem Filter.EventuallyLE.refl :
∀ {α : Type u} {β : Type v} [inst : Preorder β] (l : Filter α) (f : α → β), l.EventuallyLE f f
This theorem, named `Filter.EventuallyLE.refl`, states that for any type `α`, any type `β` equipped with a preorder relationship, any filter `l` of the type `α`, and any function `f` from `α` to `β`, the function `f` is less than or equal to itself `eventually` at the filter `l`. Here, `≤ᶠ[l]` is a notation meaning "eventually less than or equal to at filter `l`", i.e., for all elements sufficiently close to `l`, `f`'s value is less than or equal to itself. It's a reflexive property in the context of filters and functions.
More concisely: For any filter `l` on type `α`, any function `f` from `α` to a preordered type `β`, `f` is eventually less than or equal to itself at `l`, i.e., `f ≤ᶠ[l] f`.
|
Filter.empty_mem_iff_bot
theorem Filter.empty_mem_iff_bot : ∀ {α : Type u} {f : Filter α}, ∅ ∈ f ↔ f = ⊥
This theorem states that for any given type `α` and filter `f` on `α`, the empty set is an element of `f` if and only if `f` is the bottom filter. In the context of filters, the bottom filter (`⊥`) is the smallest possible filter, consisting only of the empty set.
More concisely: A filter `f` on type `α` contains the empty set if and only if `f` is the bottom filter.
|
Filter.EventuallyEq.mem_iff
theorem Filter.EventuallyEq.mem_iff :
∀ {α : Type u} {s t : Set α} {l : Filter α}, l.EventuallyEq s t → ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t
This theorem, referred to as the alias of the forward direction of `Filter.eventuallyEq_set`, states that for any type `α`, two sets `s` and `t` of type `α`, and a filter `l` on `α`, if the sets `s` and `t` are eventually equal at filter `l` (denoted as `s =ᶠ[l] t`), then for all `x` in `α` that eventually appear in `l`, `x` is in `s` if and only if `x` is in `t`. Essentially, this theorem asserts the equivalence of membership between two eventually equal sets at any point that eventually appears in a given filter.
More concisely: For any type `α`, sets `s` and `t` of type `α`, and filter `l` on `α`, if `s =ᶠ[l] t`, then for all `x` in `α`, `x` is in `s` if and only if `x` is in `t` for all `x` that eventually appear in `l`.
|
Filter.map_sup
theorem Filter.map_sup :
∀ {α : Type u} {β : Type v} {f₁ f₂ : Filter α} {m : α → β},
Filter.map m (f₁ ⊔ f₂) = Filter.map m f₁ ⊔ Filter.map m f₂
This theorem states that for any two filters `f₁` and `f₂` on a type `α`, and for any function `m` from `α` to another type `β`, the forward map of the supremum (join) of the two filters under `m` is equal to the supremum of the forward maps of the two filters individually. In other words, the operation of taking the supremum commutes with the operation of taking the forward map in this context.
More concisely: For filters `f₁` and `f₂` on type `α` and a function `m` from `α` to type `β`, `m⁁(sup f₁ f₂) = sup (m⁁f₁) (m⁁f₂)`.
|
Filter.compl_not_mem
theorem Filter.compl_not_mem : ∀ {α : Type u} {f : Filter α} {s : Set α} [inst : f.NeBot], s ∈ f → sᶜ ∉ f
The theorem `Filter.compl_not_mem` states that for any type `α`, any filter `f` on `α`, and any set `s` of type `α`, given that the filter `f` is not the bottom filter (i.e., it doesn't contain every set), if the set `s` is a member of the filter `f`, then the complement of `s` (denoted as `sᶜ`), is not a member of the filter `f`. In other words, a filter cannot contain a set and its complement at the same time, unless it is the bottom filter.
More concisely: For any filter `f` on type `α` that is not the bottom filter, and any set `s` of type `α`, if `s` is in `f`, then `sᶜ` is not in `f`.
|
Filter.map_id'
theorem Filter.map_id' : ∀ {α : Type u} {f : Filter α}, Filter.map (fun x => x) f = f
This theorem, `Filter.map_id'`, states that for any type `α` and any filter `f` of this type, the forward map of `f` using the identity function (function that maps each element to itself) is equal to `f` itself. In other words, applying the identity function to each element of a filter does not change the filter. In the language of mathematics, if we have a filter `F` on a set `A`, mapping `F` with the identity function on `A` yields `F` itself.
More concisely: For any filter `f` on type `α`, the application of the identity function maps `f` to itself, i.e., `Filter.map id f = f`.
|
Filter.NeBot.map
theorem Filter.NeBot.map :
∀ {α : Type u} {β : Type v} {f : Filter α}, f.NeBot → ∀ (m : α → β), (Filter.map m f).NeBot
This theorem states that for any types `α` and `β`, given a filter `f` on `α` that is not the bottom filter (i.e., it is not the filter containing every set), and any function `m` from `α` to `β`, the forward map of the filter `f` via the function `m` is also not the bottom filter. In other words, applying a function to a non-bottom filter does not produce a bottom filter.
More concisely: For any filter `f` on type `α` that is not the bottom filter and any function `m : α → β`, the image filter `m'' f` on `β` is also not the bottom filter.
|
Filter.mem_of_superset
theorem Filter.mem_of_superset : ∀ {α : Type u} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ f
This theorem states that for any type 'α', any filter 'f' of 'α', and any two sets 'x' and 'y' of 'α', if 'x' is a member of 'f' and 'x' is a subset of 'y', then 'y' is also a member of 'f'. In other words, if a set 'x' belongs to a filter and another set 'y' includes all elements of 'x', then 'y' also belongs to the same filter.
More concisely: If a filter 'f' of type 'α' contains a set 'x' and 'x' is a subset of another set 'y' in 'α', then 'y' is also in 'f'.
|
Filter.map_eq_bot_iff
theorem Filter.map_eq_bot_iff : ∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β}, Filter.map m f = ⊥ ↔ f = ⊥ := by
sorry
This theorem states that for any types `α` and `β`, any filter `f` of type `α`, and any mapping `m` from `α` to `β`, the forward map of the filter `f` under the mapping `m` is equal to the bottom element (the empty filter), if and only if the original filter `f` is also the bottom element. In other words, the operation of mapping a filter through a function results in an empty filter if and only if the original filter was empty.
More concisely: For any filters $f$ on type $\alpha$ and any function $m:\alpha \to \beta$, $m(f) = \bot$ if and only if $f = \bot$.
|
Filter.comap_comap
theorem Filter.comap_comap :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : Filter α} {m : γ → β} {n : β → α},
Filter.comap m (Filter.comap n f) = Filter.comap (n ∘ m) f
This theorem states that for any types `α`, `β`, and `γ`, for any filter `f` of type `α`, and for any functions `m` from `γ` to `β` and `n` from `β` to `α`, the composition of the filter `comap` function applied to `m` and then to `n` on filter `f`, is equal to the application of `comap` to the composition of `n` and `m` on filter `f`. In other words, it states that filter `comap` function is associative with function composition. This can be described in mathematical terms as `Filter.comap m (Filter.comap n f) = Filter.comap (n ∘ m) f`.
More concisely: For any filters `f` on types `α`, and functions `m: γ → β` and `n: β → α`, the composition of `Filter.comap m` and `Filter.comap n` on filter `f` equals `Filter.comap (n ∘ m) f`.
|
Filter.Tendsto.if
theorem Filter.Tendsto.if :
∀ {α : Type u} {β : Type v} {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {p : α → Prop}
[inst : (x : α) → Decidable (p x)],
Filter.Tendsto f (l₁ ⊓ Filter.principal {x | p x}) l₂ →
Filter.Tendsto g (l₁ ⊓ Filter.principal {x | ¬p x}) l₂ →
Filter.Tendsto (fun x => if p x then f x else g x) l₁ l₂
This theorem, `Filter.Tendsto.if`, states that for any types `α` and `β`, given two functions `f` and `g` mapping `α` to `β`, a predicate `p` on `α`, and two filters `l₁` on `α` and `l₂` on `β`, if `f` tends to `l₂` along the filter `l₁` intersected with the principal filter of the set of elements satisfying `p`, and `g` tends to `l₂` along the filter `l₁` intersected with the principal filter of the set of elements not satisfying `p`, then the function which maps any element `x` to `f x` if `p x` is true and `g x` otherwise, tends to `l₂` along the filter `l₁`. In simpler terms, it says that if two functions `f` and `g` tend to the same limit under different conditions defined by a predicate, then a function which is defined as `f` under the condition and `g` otherwise, also tends to the same limit.
More concisely: Given functions `f` and `g` mapping `α` to `β`, a predicate `p` on `α`, and filters `l₁` on `α` and `l₂` on `β`, if `f` tends to `l₂` along `l₁ ∩ p` and `g` tends to `l₂` along `l₁ ∩ ∘neg p`, then the function `x ↦ if p x then f x else g x` tends to `l₂` along `l₁`.
|
Filter.Eventually.comap
theorem Filter.Eventually.comap :
∀ {α : Type u} {β : Type v} {g : Filter β} {p : β → Prop},
(∀ᶠ (b : β) in g, p b) → ∀ (f : α → β), ∀ᶠ (a : α) in Filter.comap f g, p (f a)
The theorem `Filter.Eventually.comap` states that for any types `α` and `β`, given a filter `g` on `β`, a predicate `p` on `β`, if almost every element `b` of `β` in filter `g` satisfies the predicate `p`, then for any function `f` from `α` to `β`, almost every element `a` of `α` in the co-domain of `f` under the filter `g` (represented by `Filter.comap f g`), `p` holds for `f(a)`. Essentially, it assures that under certain conditions, the `eventually` property of a predicate with respect to a filter is preserved under the application of a function, using the concept of co-map.
More concisely: If a filter on `β` satisfies `p` almost everywhere, then the co-map `Filter.comap f` of a function `f` from `α` to `β` under that filter satisfies `p` almost everywhere in the image of `f` from `α`.
|
Filter.EventuallyEq.const_smul
theorem Filter.EventuallyEq.const_smul :
∀ {α : Type u} {β : Type v} {γ : Type u_2} [inst : SMul γ β] {f g : α → β} {l : Filter α},
l.EventuallyEq f g → ∀ (c : γ), l.EventuallyEq (fun x => c • f x) fun x => c • g x
This theorem states that for any types `α`, `β`, and `γ`, and given that `β` is a scalar multiple of `γ`, if two functions `f` and `g` from `α` to `β` are eventually equal at a filter `l`, then the function that multiplies `f` by any scalar `c` from `γ` will be eventually equal at the same filter `l` to the function that multiplies `g` by the same scalar `c`. In mathematical terms, if $f(x) = g(x)$ eventually at some filter $l$, then for any scalar $c$, $c \cdot f(x) = c \cdot g(x)$ eventually at the same filter $l$.
More concisely: For any types `α`, `β` being scalar types with `β = c * γ` for some scalar `c`, if functions `f` and `g` from `α` to `β` are eventually equal at filter `l`, then `c * f(x)` is eventually equal to `c * g(x)` at the same filter `l`.
|
Filter.range_mem_map
theorem Filter.range_mem_map : ∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β}, Set.range m ∈ Filter.map m f
This theorem states that for any two types `α` and `β`, any filter `f` of type `α`, and any function `m` from `α` to `β`, the range of the function `m` (i.e., the set of all output values `m` can produce) is an element of the filter obtained by mapping function `m` over the filter `f`. In other words, every value that the function `m` can produce, when applied to the elements of the filter `f`, will exist in the output of the filter mapping operation.
More concisely: For any filter `f` on type `α` and function `m` from `α` to `type β`, the range of `m` is included in the image of `m` applied to `f`.
|
Filter.not_frequently
theorem Filter.not_frequently :
∀ {α : Type u} {p : α → Prop} {f : Filter α}, (¬∃ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, ¬p x
This theorem states that for any type `α`, predicate `p` on `α`, and filter `f` on `α`, the property of "it is not the case that there frequently exists an `x` in `f` such that `p x` holds" is equivalent to "for all `x` frequently in `f`, `p x` does not hold". Mathematically speaking, this theorem is expressing a property about negation and quantifiers in the context of filters.
More concisely: For any type `α`, predicate `p` on `α`, and filter `f` on `α`, the property "there is no dense subset of `f` on which `p` holds" is equivalent to "for all `x` in the dense subset of `f`, `p x` does not hold".
|
Mathlib.Order.Filter.Basic._auxLemma.21
theorem Mathlib.Order.Filter.Basic._auxLemma.21 : ∀ {α : Type u} {f : Filter α}, f.NeBot = (f ≠ ⊥)
This theorem states that for any given type `α` and any filter `f` of this type, the property that `f` is not a trivial (or "bottom") filter is equivalent to the assertion that `f` is not equal to the bottom filter. In other words, a filter `f` on `α` is non-trivial if and only if `f` is not equal to the trivial filter.
More concisely: A filter `f` on type `α` is non-trivial if and only if it is not equal to the bottom filter.
|
Filter.principal_mono
theorem Filter.principal_mono : ∀ {α : Type u} {s t : Set α}, Filter.principal s ≤ Filter.principal t ↔ s ⊆ t := by
sorry
The theorem `Filter.principal_mono` states that for any type `α` and any two sets `s` and `t` of type `α`, the principal filter of `s` is less than or equal to the principal filter of `t` if and only if `s` is a subset of `t`. In other words, the containment relationship between the principal filters of two sets directly corresponds to the subset relationship between the two sets themselves.
More concisely: The principal filters of sets `s` and `t` over type `α` are equal if and only if `s` is a subset of `t`.
|
Filter.biInter_mem
theorem Filter.biInter_mem :
∀ {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} {is : Set β},
is.Finite → (⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f)
The theorem `Filter.biInter_mem` states that for any type `α`, any filter `f` of `α`, any type `β`, and any function `s` mapping from `β` to a set of `α`, and any set `is` of `β`, if the set `is` is finite, then the intersection over all `i` in `is` of the sets `s i` belongs to the filter `f` if and only if for all `i` in `is`, the set `s i` belongs to the filter `f`. In other words, all the sets `s i` for `i` in `is` are in the filter `f` if and only if their intersection is also in `f`, when `is` is a finite set.
More concisely: If `f` is a filter on type `α`, `s` is a function from type `β` to `α`, and `is` is a finite set of `β`, then `∩ (map s is) ∈ f` if and only if `s i ∈ f` for all `i` in `is`.
|
Filter.map_comap_of_surjective
theorem Filter.map_comap_of_surjective :
∀ {α : Type u} {β : Type v} {f : α → β},
Function.Surjective f → ∀ (l : Filter β), Filter.map f (Filter.comap f l) = l
The theorem `Filter.map_comap_of_surjective` states that for any types α and β, and any function `f` from α to β, if `f` is a surjective function (i.e., for every element `b` in β, there is some element `a` in α such that `f(a) = b`), then for any filter `l` on β, mapping `l` under `f` after applying the co-domain filter of `f` to `l` is equal to the original filter `l`. In simpler terms, this theorem implies that for a surjective function, the process of mapping the filter after applying the comap operation to the filter results in the original filter.
More concisely: For any surjective function `f` between types α and β, `filter.map (f)` equals `filter.coe_filter (filter.map (subtype.val f)) (filter.map (subtype.coe) l)` for any filter `l` on β.
|
Mathlib.Order.Filter.Basic._auxLemma.147
theorem Mathlib.Order.Filter.Basic._auxLemma.147 :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop}, (∃ b, (∃ a, f a = b) ∧ p b) = ∃ a, p (f a)
This theorem states that for any types `α` and `β` and any function `f` from `α` to `β`, the property that there exists a value `b` of type `β` such that `b` is the image of some value `a` of type `α` under `f` and `b` satisfies a property `p`, is equivalent to the property that there exists a value `a` of type `α` such that `f(a)` satisfies the property `p`. In other words, it's expressing that the existence of an element in the codomain satisfying a property can be traced back to the existence of an element in the domain such that its image under the function satisfies that property.
More concisely: For any functions between types and properties, the existence of an image satisfying a property is equivalent to the existence of a preimage with that property.
|
Mathlib.Order.Filter.Basic._auxLemma.43
theorem Mathlib.Order.Filter.Basic._auxLemma.43 :
∀ {α : Type u} {f g : Filter α} {s : Set α}, (s ∈ f ⊓ g) = ∃ t₁ ∈ f, ∃ t₂ ∈ g, s = t₁ ∩ t₂
The theorem `Mathlib.Order.Filter.Basic._auxLemma.43` states that for any type `α`, any two filters `f` and `g` on `α`, and any set `s` of `α`, the set `s` is in the intersection of the filters `f` and `g` if and only if there exists some set `t₁` in filter `f` and some set `t₂` in filter `g` such that `s` is the intersection of `t₁` and `t₂`.
More concisely: For filters ${f, g}$ on type ${α}$, and ${s \subseteq α}$, ${s} \in {f} \cap {g}$ if and only if there exist ${{t₁} \in {f}}$ and ${{t₂} \in {g}}$ such that ${s = t₁ ∩ t₂}$.
|
Filter.disjoint_comap
theorem Filter.disjoint_comap :
∀ {α : Type u} {β : Type v} {g₁ g₂ : Filter β} {m : α → β},
Disjoint g₁ g₂ → Disjoint (Filter.comap m g₁) (Filter.comap m g₂)
This theorem asserts that if two filters `g₁` and `g₂` on a type `β` are disjoint (in the sense that their infimum is the bottom element in the lattice of filters), then the filters obtained by precomposing these filters with a function `m` from some other type `α` to `β` (i.e., the filters `Filter.comap m g₁` and `Filter.comap m g₂`) are also disjoint. This means that for any element in the filter obtained by the composition, if it is less than or equal to both `Filter.comap m g₁` and `Filter.comap m g₂`, it is less than or equal to the bottom element of the filter lattice.
More concisely: If filters `g₁` and `g₂` on type `β` are disjoint, then the filters obtained by composing them with a function `m` from type `α` to `β` (`Filter.comap m g₁` and `Filter.comap m g₂`) are also disjoint, meaning their infimum is the bottom element in the lattice of filters.
|
Filter.eventuallyEq_set
theorem Filter.eventuallyEq_set :
∀ {α : Type u} {s t : Set α} {l : Filter α}, l.EventuallyEq s t ↔ ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t
This theorem states that for any given type `α`, any two sets `s` and `t` of type `α`, and any filter `l` over `α`, the condition of `s` being eventually equal to `t` given the filter `l` (denoted by `s =ᶠ[l] t`) is equivalent to the condition that for all elements `x` of type `α` that "eventually" lie in the filter `l` (expressed by the `∀ᶠ (x : α) in l` notation), `x` belongs to set `s` if and only if `x` belongs to set `t`. Essentially, it says that two sets are eventually equal under some filter if and only if, under that filter, membership in one set implies membership in the other set (and vice versa) for all elements "eventually".
More concisely: For any type `α`, sets `s` and `t` of type `α`, and filter `l` over `α`, sets `s` and `t` are eventually equal under filter `l` if and only if for all `x` in `l`, `x` is in `s` if and only if `x` is in `t`.
|
Mathlib.Order.Filter.Basic._auxLemma.166
theorem Mathlib.Order.Filter.Basic._auxLemma.166 :
∀ {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
Filter.Tendsto f l₁ l₂ = ∀ s ∈ l₂, ∀ᶠ (x : α) in l₁, f x ∈ s
The theorem `Mathlib.Order.Filter.Basic._auxLemma.166` states that for any types `α` and `β`, and for any function `f` from `α` to `β`, and for any filters `l₁` on `α` and `l₂` on `β`, the statement "Filter `l₁` tends to filter `l₂` under function `f`" is equivalent to the statement "For every set `s` in the filter `l₂`, all elements `x` from the filter `l₁` eventually map under `f` into the set `s`. Here, `∀ᶠ (x : α) in l₁, f x ∈ s` is denoting the "eventually" quantifier, signifying that from some point onward in filter `l₁`, all elements `x` satisfy the condition `f x ∈ s`.
More concisely: For filters \(l\_1\) on type \(\alpha\) and \(l\_2\) on type \(\beta\), and a function \(f : \alpha \rightarrow \beta\), the filters \(l\_1\) tends to \(l\_2\) under \(f\) if and only if for every set \(s \in l\_2\), all elements \(x \in l\_1\) eventually map under \(f\) into \(s\).
|
Filter.mem_comap_prod_mk
theorem Filter.mem_comap_prod_mk :
∀ {α : Type u} {β : Type v} {x : α} {s : Set β} {F : Filter (α × β)},
s ∈ Filter.comap (Prod.mk x) F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F
This theorem, `Filter.mem_comap_prod_mk`, states that for any types `α` and `β`, any element `x : α`, any set `s : Set β`, and any filter `F : Filter (α × β)`, the set `s` is in the preimage of `F` under the function `Prod.mk x` if and only if the set of pairs `p` such that if the first element of `p` equals `x`, then the second element of `p` is in `s`, is in `F`. This theorem plays a role in the definition of `UniformSpace`, where it is used in its right-hand-side form.
More concisely: For any types `α` and `β`, filter `F` on `α × β`, `x : α`, and set `s : Set β`, `s ∈ F .| (Prod.mk x)` if and only if `{(x, y) | y ∈ s} ∈ F`.
|
Filter.EventuallyEq.trans
theorem Filter.EventuallyEq.trans :
∀ {α : Type u} {β : Type v} {l : Filter α} {f g h : α → β},
l.EventuallyEq f g → l.EventuallyEq g h → l.EventuallyEq f h
This theorem, `Filter.EventuallyEq.trans`, states that for any given types `α` and `β`, any filter `l` on type `α`, and any three functions `f`, `g`, and `h` from `α` to `β`, if `f` is eventually equal to `g` with respect to the filter `l`, and `g` is eventually equal to `h` with respect to the same filter `l`, then `f` is eventually equal to `h` with respect to filter `l`. This is a transitivity property of the "eventually equal" relation in the context of filters.
More concisely: If filters `l` on types `α` make functions `f` and `g` from `α` to `β` eventually equal, then `f` and `h` are eventually equal with respect to filter `l` if `g` is eventually equal to `h` with respect to `l`.
|
Filter.eventually_iff
theorem Filter.eventually_iff : ∀ {α : Type u} {f : Filter α} {P : α → Prop}, (∀ᶠ (x : α) in f, P x) ↔ {x | P x} ∈ f
This theorem states that, for any type 'α', any filter 'f' on 'α', and any proposition 'P' about elements of 'α', the proposition 'P' holds eventually for some element 'x' in the filter 'f' if and only if the set of elements 'x' for which 'P' holds is in the filter 'f'. In other words, 'P' happens eventually in 'f' means the set of all values satisfying 'P' belongs to 'f'.
More concisely: For any filter $f$ on a type $\alpha$ and proposition $P$ about elements of $\alpha$, $P$ holds eventually for some $x$ in $f$ if and only if the set of $x$ with $P(x)$ is in $f$.
|
Filter.eventually_and
theorem Filter.eventually_and :
∀ {α : Type u} {p q : α → Prop} {f : Filter α},
(∀ᶠ (x : α) in f, p x ∧ q x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in f, q x
This theorem states that, for any type `α`, predicates `p` and `q`, and filter `f` on `α`, the property of `p` and `q` holding "eventually" (that is, at all points in the filter beyond a certain point) is equivalent to `p` holding eventually and `q` holding eventually individually. In other words, both `p` and `q` will be true for all elements in the filter `f` beyond a certain point if and only if each of `p` and `q` individually is true for all elements in the filter beyond a certain point.
More concisely: For any type `α`, predicates `p` and `q`, and filter `f` on `α`, the properties of `p` and `q` holding eventually in `f` are equivalent.
|
Filter.Tendsto.inf
theorem Filter.Tendsto.inf :
∀ {α : Type u} {β : Type v} {f : α → β} {x₁ x₂ : Filter α} {y₁ y₂ : Filter β},
Filter.Tendsto f x₁ y₁ → Filter.Tendsto f x₂ y₂ → Filter.Tendsto f (x₁ ⊓ x₂) (y₁ ⊓ y₂)
The theorem `Filter.Tendsto.inf` states that for any types `α` and `β`, for any function `f` mapping `α` to `β`, and for any filters `x₁`, `x₂` on `α` and `y₁`, `y₂` on `β`, if `f` is tending towards `y₁` under filter `x₁` and tending towards `y₂` under filter `x₂`, then `f` is also tending towards the infimum of `y₁` and `y₂` under the infimum of `x₁` and `x₂`. In mathematical terms, if $f$ tends to $y₁$ when $x$ tends to $x₁$ and $f$ tends to $y₂$ when $x$ tends to $x₂$, then $f$ tends to the intersection of $y₁$ and $y₂$ when $x$ tends to the intersection of $x₁$ and $x₂$.
More concisely: If functions $f$ tends to $y\_1$ with respect to filter $x\_1$ and tends to $y\_2$ with respect to filter $x\_2$, then $f$ tends to the inf infimum of $y\_1$ and $y\_2$ with respect to the infimum of $x\_1$ and $x\_2$.
|
Mathlib.Order.Filter.Basic._auxLemma.78
theorem Mathlib.Order.Filter.Basic._auxLemma.78 : ∀ {α : Type u} {p : α → Prop}, (∀ᶠ (x : α) in ⊥, p x) = True := by
sorry
This theorem, `Mathlib.Order.Filter.Basic._auxLemma.78`, states that for any type 'α' and any predicate 'p' defined on 'α', the assertion that the predicate 'p' holds for all elements 'x' of type 'α' in the bottom filter (denoted by ⊥) is always true. The bottom filter (⊥) in this context is the smallest filter, which contains no elements, hence every statement about its elements is vacuously true.
More concisely: For any type 'α' and predicate 'p' on 'α', the statement 'p' holds for all elements in the bottom filter (⊥) is vacuously true.
|
Filter.nonempty_of_mem
theorem Filter.nonempty_of_mem : ∀ {α : Type u} {f : Filter α} [hf : f.NeBot] {s : Set α}, s ∈ f → s.Nonempty := by
sorry
The theorem `Filter.nonempty_of_mem` states that for any type `α`, any filter `f` of type `α` such that `f` is not the bottom filter (expressed via the `Filter.NeBot f` assumption), and any set `s` of type `α`, if `s` belongs to the filter `f` (expressed as `s ∈ f`), then the set `s` is not empty (expressed as `Set.Nonempty s`). In other words, if a set is in a non-bottom filter, it must contain at least one element.
More concisely: If `α` is a type, `f` is a non-bottom filter on `α`, and `s ∈ f`, then `Set.Nonempty s`.
|
Mathlib.Order.Filter.Basic._auxLemma.15
theorem Mathlib.Order.Filter.Basic._auxLemma.15 :
∀ {α : Type u} {s : Set α} {f : Filter (Filter α)}, (s ∈ f.join) = ({t | s ∈ t} ∈ f)
The theorem `Mathlib.Order.Filter.Basic._auxLemma.15` states that for any type `α`, any set `s` of type `α`, and any filter `f` on the type `Filter α` (that is, a filter of filters), the set `s` is an element of the filter obtained by joining `f` if and only if the set of all filters `t` such that `s` is an element of `t` is an element of `f`. This is essentially the defining property of the join operation on filters of filters.
More concisely: A set belongs to the join of filters if and only if it is an element of every filter in the joining family.
|
Mathlib.Order.Filter.Basic._auxLemma.26
theorem Mathlib.Order.Filter.Basic._auxLemma.26 :
∀ {α : Type u} {f g : Filter α} {s : Set α}, (s ∈ f ⊔ g) = (s ∈ f ∧ s ∈ g)
This theorem states that for any type `α`, any filters `f` and `g` on this type, and any set `s` of elements of this type, `s` being an element in the join (supremum) of the filters `f` and `g` is equivalent to `s` being an element both in `f` and in `g`. In other words, a set is in the join of two filters if and only if it is in both filters.
More concisely: For any type `α`, filters `f` and `g` on `α`, and set `s` in `α`, `s` belongs to the join of filters `f` and `g` if and only if `s` belongs to both `f` and `g` (i.e., `s` is in `f` and `g`).
|
Filter.tendsto_id'
theorem Filter.tendsto_id' : ∀ {α : Type u} {x y : Filter α}, Filter.Tendsto id x y ↔ x ≤ y
The theorem `Filter.tendsto_id'` states that for any types `α` and for any filters `x` and `y` on `α`, the identity function `id` tends to move points in `x` towards `y` if and only if `x` is less than or equal to `y`. In other words, for each neighborhood in `y`, its preimage under the identity function is a neighborhood in `x`, exactly when `x` is a subset of `y`. This theorem connects the concept of filter tendsto (or limit) with the order relation on filters.
More concisely: The identity function maps filter `x` to `y` strongly, i.e., `x ⊆ y` if and only if the identity function tends to map elements in `x` to `y`.
|
Filter.eventually_all
theorem Filter.eventually_all :
∀ {α : Type u} {ι : Sort u_2} [inst : Finite ι] {l : Filter α} {p : ι → α → Prop},
(∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x
This theorem, `Filter.eventually_all`, states that, for any type `α`, any sort `ι` (where `ι` is finite), any filter `l` on `α`, and any property `p` from `ι` to `α` to a proposition, the following two statements are equivalent:
1. For every value `x` from `α` that eventually appears in the filter `l`, the property `p` holds for all `i` from `ι`.
2. For each `i` from `ι`, the property `p` holds for every value `x` from `α` that eventually appears in the filter `l`.
In other words, we can switch the order of the universal quantifiers without changing the meaning of the statement when discussing properties that eventually hold in a filter.
More concisely: For any type `α`, filter `l` on `α`, finite sort `ι`, and property `p` from `ι` to `α` to a proposition, `p` holds for all eventually filtered elements if and only if it holds for every eventually filtered element for each `i` in `ι`.
|
Filter.le_def
theorem Filter.le_def : ∀ {α : Type u} {f g : Filter α}, f ≤ g ↔ ∀ x ∈ g, x ∈ f
This theorem, `Filter.le_def`, is about filters in a certain type `α`. A filter `f` is less than or equal to a filter `g` if and only if for every set `x` that belongs to the filter `g`, `x` also belongs to the filter `f`. In other words, filter `f` is a subset of filter `g` when every set in `g` is also found in `f`.
More concisely: A filter `f` is less than or equal to a filter `g` if and only if every element in `g` belongs to `f`.
|
Mathlib.Order.Filter.Basic._auxLemma.119
theorem Mathlib.Order.Filter.Basic._auxLemma.119 :
∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {P : β → Prop},
(∃ᶠ (b : β) in Filter.map m f, P b) = ∃ᶠ (a : α) in f, P (m a)
This theorem states that for any types `α` and `β`, any filter `f` on `α`, any function `m` from `α` to `β`, and any property `P` on `β`, the condition "there eventually exists an element `b` in the filter obtained by applying the function `m` to `f` such that `P b` holds" is equivalent to the condition "there eventually exists an element `a` in `f` such that `P (m a)` holds". In other words, whether we check the property `P` after or before applying the function `m` doesn't change the eventual elements for which `P` holds.
More concisely: For any filters `f` on type `α`, functions `m` from `α` to type `β`, and properties `P` on `β`, the filters `m '' f` and `{x | ∃y ∈ f, P y ∧ m x = y}` have the same eventual elements.
|
Filter.tendsto_principal_principal
theorem Filter.tendsto_principal_principal :
∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} {t : Set β},
Filter.Tendsto f (Filter.principal s) (Filter.principal t) ↔ ∀ a ∈ s, f a ∈ t
This theorem, `Filter.tendsto_principal_principal`, asserts that for any types `α` and `β`, any function `f` from `α` to `β`, and any sets `s` of `α` and `t` of `β`, the function `f` tends to the principal filter of `t` from the principal filter of `s` if and only if for all elements `a` in `s`, the image of `a` under `f` is in `t`. In other words, the theorem states that a function `f` tends towards the filter generated by `t` when it is restricted to the filter generated by `s`, if and only if every element of `s` gets mapped to an element in `t` by the function `f`. Here, a filter generated by a set is the collection of all supersets of the set, and a function tends towards a filter if the preimage of every neighborhood in the target filter is a neighborhood in the source filter.
More concisely: A function from one set to another tends to the principal filter of its image set if and only if every element in the domain set is mapped to an element in the image set.
|
Filter.coext
theorem Filter.coext : ∀ {α : Type u} {f g : Filter α}, (∀ (s : Set α), sᶜ ∈ f ↔ sᶜ ∈ g) → f = g
The theorem, `Filter.coext`, is an extensionality lemma for filters in Lean 4. For any type `α` and any two filters `f` and `g` on `α`, it states that if for every set `s` of `α`, the complement of `s` belongs to `f` if and only if it belongs to `g`, then `f` and `g` are the same filter. This theorem can be particularly useful for filters such as `Filter.comap`, `Filter.coprod`, `Filter.Coprod`, and `Filter.cofinite`, which have good lemmas about the membership of a set's complement in the filter.
More concisely: Two filters on a type `α` are equal if and only if their complements of sets have the same membership relation.
|
Filter.monotone_principal
theorem Filter.monotone_principal : ∀ {α : Type u}, Monotone Filter.principal
The theorem `Filter.monotone_principal` states that for any given type `α`, the function `Filter.principal` is monotone. This means that if we have two sets `a` and `b` of type `α` such that `a` is a subset of `b`, then the principal filter of `a` is a subset of the principal filter of `b`. In other words, the creation of principal filters by the function `Filter.principal` respects the order of the input sets, making it monotone.
More concisely: For any type `α` and sets `a` and `b` of type `α`, if `a` is a subset of `b`, then `Filter.principal a` is a subset of `Filter.principal b`.
|
Filter.EventuallyEq.le
theorem Filter.EventuallyEq.le :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f g : α → β},
l.EventuallyEq f g → l.EventuallyLE f g
This theorem states that for any types `α` and `β`, with `β` being a Preorder, and any filter `l` on `α`, if two functions `f` and `g` from `α` to `β` are eventually equal at `l`, then `f` is eventually less than or equal to `g` at `l`. In other words, if `f` and `g` are the same for all inputs beyond a certain point in the domain defined by the filter `l`, then `f` is also less than or equal to `g` for all inputs beyond that point.
More concisely: Given types `α` and a preorder `β`, if functions `f` and `g` from `α` to `β` agree on a filter `l`'s elements, then `f ≤ g` holds for all `x ∈ ∃ (l)`.
|
Mathlib.Order.Filter.Basic._auxLemma.171
theorem Mathlib.Order.Filter.Basic._auxLemma.171 :
∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α}, (a ≤ iInf f) = ∀ (i : ι), a ≤ f i
This theorem states that for any type `α` that forms a complete lattice, and any function `f` from an arbitrary type `ι` to `α`, along with a given value `a` of type `α`, `a` is less than or equal to the infimum of `f` if and only if `a` is less than or equal to `f i` for every `i` of type `ι`. The infimum of `f` is calculated over its range using the `iInf` function.
More concisely: For any complete lattice `α` and function `f` from type `ι` to `α`, and `a` in `α`, `a` is the infimum of `f` if and only if `a` is less than or equal to `f(i)` for all `i` in `ι`.
|
Filter.EventuallyEq.union
theorem Filter.EventuallyEq.union :
∀ {α : Type u} {s t s' t' : Set α} {l : Filter α},
l.EventuallyEq s t → l.EventuallyEq s' t' → l.EventuallyEq (s ∪ s') (t ∪ t')
The theorem `Filter.EventuallyEq.union` states that for any type `α`, any sets `s`, `t`, `s'`, `t'` of type `α`, and any filter `l` on `α`, if `s` is eventually equal to `t` with respect to the filter `l` and `s'` is eventually equal to `t'` with respect to the same filter `l`, then the union of sets `s` and `s'` is eventually equal to the union of sets `t` and `t'` with respect to the filter `l`. Here, "eventually equal" means that outside a set of some measure (which is ignored), the two sets are equal.
More concisely: If sets $s$, $t$, $s'$, $t'$ of type $\alpha$ satisfy $s \equiv_\infty t$ and $s' \equiv_\infty t'$ with respect to filter $l$ on $\alpha$, then $s \cup s' \equiv_\infty t \cup t'$. Here, $\equiv_\infty$ denotes eventual equality.
|
Filter.frequently_of_forall
theorem Filter.frequently_of_forall :
∀ {α : Type u} {f : Filter α} [inst : f.NeBot] {p : α → Prop}, (∀ (x : α), p x) → ∃ᶠ (x : α) in f, p x
This theorem states that for any type `α`, any filter `f` on `α` that is not the bottom filter, and any predicate `p` on `α`, if the predicate `p` holds for all elements `x` of the type `α`, then there exists a subset of elements from `f` for which `p` holds frequently. In other words, if a property is true for all elements, then there are many places in the filter where it's true.
More concisely: If `f` is a non-bottom filter on type `α` and `p` is a predicate on `α` such that `∀x ∈ α, p x`, then there exists a non-empty `X ∈ f` such that `#{x ∈ X | p x} / #X ≥ ε` for some constant `ε > 0`.
|
Mathlib.Order.Filter.Basic._auxLemma.179
theorem Mathlib.Order.Filter.Basic._auxLemma.179 : ∀ {α : Type u} {a b : α}, (a ∈ {b}) = (a = b)
This theorem, `Mathlib.Order.Filter.Basic._auxLemma.179`, states that for any type α, and any two instances a and b of this type, a is an element of the singleton set {b} if and only if a is equal to b. In other words, given any type and instances a and b of that type, a being in the set {b} is equivalent to a being equal to b.
More concisely: For any type α and instances a, b of α, a is in the singleton set {b} if and only if a is equal to b.
|
Filter.NeBot.mono
theorem Filter.NeBot.mono : ∀ {α : Type u} {f g : Filter α}, f.NeBot → f ≤ g → g.NeBot
This theorem states that for any two filters `f` and `g` of some type `α`, if `f` is not a bottom filter and `f` is less than or equal to `g` (meaning every set in `f` is also in `g`), then `g` is also not a bottom filter. This theorem is essentially asserting a form of monotonicity for non-bottom filters.
More concisely: If `f` is a non-bottom filter on type `α` and `f` is subset of filter `g`, then `g` is also a non-bottom filter.
|
Filter.mem_of_eq_bot
theorem Filter.mem_of_eq_bot : ∀ {α : Type u} {f : Filter α} {s : Set α}, f ⊓ Filter.principal sᶜ = ⊥ → s ∈ f := by
sorry
This theorem states that for any type `α`, any filter `f` of type `α`, and any set `s` of type `α`, if the intersection of filter `f` and the principal filter of the complement of set `s` equals the bottom element (`⊥`, representing the smallest filter or an empty filter), then set `s` is a member of filter `f`. Essentially, it's saying that if filtering out everything outside of `s` from `f` leaves nothing, then `s` must have been part of `f` to begin with.
More concisely: If the intersection of filter `f` on type `α` with the complement of set `s` is the bottom filter, then `s` is an element of `f`.
|
Filter.iInf_neBot_of_directed
theorem Filter.iInf_neBot_of_directed :
∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} [hn : Nonempty α],
Directed (fun x x_1 => x ≥ x_1) f → (∀ (i : ι), (f i).NeBot) → (iInf f).NeBot
The theorem `Filter.iInf_neBot_of_directed` states that if we have a directed family of filters `f : ι → Filter α` on a nonempty type `α`, and if none of the filters in this family are the bottom filter, then the indexed infimum of the family, `iInf f`, is also not the bottom filter. Here, a family of filters is said to be directed if, for any two filters in the family, there exists a third filter that is greater than or equal to both. This theorem also has a variant `iInf_neBot_of_directed'` which assumes that the index set `ι` is nonempty instead of the type `α`.
More concisely: If `α` is nonempty and `f : ι → Filters α` is a directed family of filters on `α` with no bottom filter, then `iInf f` is also not the bottom filter.
|
Filter.le_generate_iff
theorem Filter.le_generate_iff : ∀ {α : Type u} {s : Set (Set α)} {f : Filter α}, f ≤ Filter.generate s ↔ s ⊆ f.sets
This theorem states that for any type `α`, any set of sets `s` of type `α`, and any filter `f` on `α`, the filter `f` is less than or equal to the filter `generate s` if and only if `s` is a subset of the sets in `f`. In other words, the filter `f` is contained within the filter generated by `s` exactly when all sets in `s` are also in `f`.
More concisely: For any type `α`, filter `f` on `α`, and set of sets `s` over `α`, `f ⊆ generate s` if and only if `s ⊆ f`.
|
Mathlib.Order.Filter.Basic._auxLemma.49
theorem Mathlib.Order.Filter.Basic._auxLemma.49 :
∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, ((∃ x, p x) → b) = ∀ (x : α), p x → b
This theorem states that for any type `α`, any proposition `p` about `α`, and any proposition `b`, the statement "if there exists an `x` of type `α` that satisfies `p`, then `b` must be true" is equivalent to the statement "for all `x` of type `α`, if `x` satisfies `p`, then `b` must be true". Essentially, it captures the logical equivalence between an existential quantifier in the antecedent of an implication and a universal quantifier in the hypothesis of the implication.
More concisely: For any type `α`, proposition `p` about `α`, and proposition `b`, the existential quantifier "∃x : α. p(x)" is logically equivalent to the universal quantifier "∀x : α. p(x) → b".
|
Mathlib.Order.Filter.Basic._auxLemma.181
theorem Mathlib.Order.Filter.Basic._auxLemma.181 :
∀ {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
Filter.Tendsto f l₁ l₂ = ∀ s ∈ l₂, f ⁻¹' s ∈ l₁
This theorem states that for any two types `α` and `β`, a function `f` from `α` to `β`, and two filters `l₁` and `l₂` on `α` and `β` respectively, the function `f` tends to the filter `l₂` from `l₁` if and only if for every set `s` in `l₂`, the preimage of `s` under the function `f` is in `l₁`. In other words, a function `f` has a limit at a point if every neighborhood of the limit point in the codomain has a preimage that is a neighborhood of the point in the domain.
More concisely: A function between two types has a limit from one filter to another if and only if the preimage of every set in the target filter is in the domain filter.
|
Filter.mem_inf_principal
theorem Filter.mem_inf_principal :
∀ {α : Type u} {f : Filter α} {s t : Set α}, s ∈ f ⊓ Filter.principal t ↔ {x | x ∈ t → x ∈ s} ∈ f
This theorem, `Filter.mem_inf_principal`, states that for any type `α`, any filter `f` on `α`, and any two sets `s` and `t` of `α`, the set `s` is in the intersection of the filter `f` and the principal filter of `t` if and only if the set of all elements `x` such that `x` is in `t` implies `x` is in `s`, belongs to the filter `f`. In other words, it establishes an equivalence between the membership of `s` in the intersection of `f` and the principal filter of `t`, and the membership of a set of certain elements in `f`, where these elements are those that, if they are in `t`, then they must also be in `s`.
More concisely: For any filter `f` on a type `α` and sets `s` and `t` of `α`, `s` belongs to the intersection of `f` and the principal filter of `t` if and only if the set of elements in `t` that lie in `s` is an element of `f`.
|
Mathlib.Order.Filter.Basic._auxLemma.68
theorem Mathlib.Order.Filter.Basic._auxLemma.68 : ∀ {α : Type u} (f : Filter α), (∀ᶠ (x : α) in f, True) = True := by
sorry
The theorem `Mathlib.Order.Filter.Basic._auxLemma.68` states that for any type `α` and any filter `f` of type `α`, the statement that "for all `x` of type `α` in the filter `f`, the proposition `True` holds" is itself always True. In other words, it's always the case that for any element in any filter, the proposition `True` is true.
More concisely: For any type `α` and filter `f` on `α`, the proposition that all elements in `f` satisfy `True` is always true.
|
Filter.eventually_congr
theorem Filter.eventually_congr :
∀ {α : Type u} {f : Filter α} {p q : α → Prop},
(∀ᶠ (x : α) in f, p x ↔ q x) → ((∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, q x)
This theorem, `Filter.eventually_congr`, states that for any type `α`, any `Filter α` called `f`, and any two propositions `p` and `q` about `α`, if it is eventually the case in `f` that `p x` is equivalent to `q x` for all `x` of type `α`, then it is true that `p x` is eventually the case in `f` if and only if `q x` is eventually the case in `f`. In simpler terms, if two conditions `p` and `q` are eventually equivalent in a certain context (the filter `f`), then an event described by `p` happens eventually in this context if and only if an event described by `q` does.
More concisely: If two propositions `p` and `q` are eventually equivalent in a filter `f` over type `α`, then `p` and `q` have equivalent eventually subsets in `f`.
|
Mathlib.Order.Filter.Basic._auxLemma.47
theorem Mathlib.Order.Filter.Basic._auxLemma.47 :
∀ {α : Sort u_1} {p : α → Prop} {q : { a // p a } → Prop}, (∃ x, q x) = ∃ a, ∃ (b : p a), q ⟨a, b⟩
This theorem states that for any type `α`, any property `p` of `α`, and any property `q` of `a` such that `a` satisfies `p`, stating that there exists an `x` that satisfies `q` is equivalent to stating that there exists an `a` and a proof `b` that `a` satisfies `p` such that `q` holds for `a` with the given proof `b`. In other words, it defines how existential quantification interacts with the subtype construction in Lean.
More concisely: For any type `α`, property `p` of `α`, and property `q` of `a` satisfying `p`, the existence of an `x` with `q` is equivalent to the existence of `a` with `p` and a proof `b` such that `a` has property `p` and `q` holds for `a` with proof `b`.
|
Filter.neBot_iff
theorem Filter.neBot_iff : ∀ {α : Type u} {f : Filter α}, f.NeBot ↔ f ≠ ⊥
This theorem states that, for any given type `α` and a filter `f` on this type, the filter `f` is not minimal (or equivalently, is non-trivial or contains more than the empty set) if and only if `f` is not equal to the bottom element (denoted by ⊥). Here, the bottom element represents the smallest possible filter, which, in this context, is a filter that contains only the empty set. This theorem establishes an equivalence between the `Filter.NeBot` predicate and the inequality `f ≠ ⊥`, both of which are ways to express that a filter is non-trivial in Lean 4.
More concisely: A filter `f` over type `α` is non-trivial if and only if it is not equal to the bottom filter (denoted by ⊥).
|
Filter.inf_principal_eq_bot
theorem Filter.inf_principal_eq_bot : ∀ {α : Type u} {f : Filter α} {s : Set α}, f ⊓ Filter.principal s = ⊥ ↔ sᶜ ∈ f
The theorem `Filter.inf_principal_eq_bot` states that for any type `α`, any filter `f` on `α`, and any set `s` of `α`, the infimum (i.e., the greatest lower bound) of `f` and the principal filter of `s` is the bottom element (i.e., the smallest element of the ordered set of filters) if and only if the complement of `s` is an element of `f`. The "principal filter of `s`" refers to the collection of all supersets of `s`, and the "complement of `s`" (denoted `sᶜ`) is the set of all elements not in `s`.
More concisely: For any filter `f` on type `α` and set `s`, the infimum of `f` and the principal filter of `s` equals the bottom element if and only if the complement of `s` is an element of `f`.
|
Filter.EventuallyLE.inter
theorem Filter.EventuallyLE.inter :
∀ {α : Type u} {s t s' t' : Set α} {l : Filter α},
l.EventuallyLE s t → l.EventuallyLE s' t' → l.EventuallyLE (s ∩ s') (t ∩ t')
The theorem `Filter.EventuallyLE.inter` states that for any type `α`, any sets `s`, `t`, `s'`, `t'` of type `α`, and any filter `l` over `α`, if `s` is eventually less than or equal to `t` under filter `l` and `s'` is eventually less than or equal to `t'` under filter `l`, then the intersection of `s` and `s'` is eventually less than or equal to the intersection of `t` and `t'` under the same filter `l`. In more intuitive terms, this theorem is about the relationship between two events that are both eventually true according to some filter: if each event individually implies another event, then the intersection of the original events implies the intersection of the resulting events.
More concisely: If filters `l` make sets `s` eventually included in `t` and sets `s'` eventually included in `t'`, then the intersection of `s` and `s'` is eventually included in the intersection of `t` and `t'`.
|
Filter.Eventually.and_frequently
theorem Filter.Eventually.and_frequently :
∀ {α : Type u} {p q : α → Prop} {f : Filter α},
(∀ᶠ (x : α) in f, p x) → (∃ᶠ (x : α) in f, q x) → ∃ᶠ (x : α) in f, p x ∧ q x
This theorem states that for any type `α` and two properties `p` and `q` defined on `α`, along with a filter `f` on `α`, if it is true that for every value `x` from `α` that eventually appears in the filter `f`, `p x` holds, and there exists some value `x` from `α` that frequently appears in the filter `f` for which `q x` holds, then there exists some value `x` from `α` that frequently appears in the filter `f` for which both `p x` and `q x` hold.
More concisely: If for all `x` in a type `α` that are eventually in a filter `f`, property `p(x)` holds, and there exists `x` in `α` with frequency in `f` such that `q(x)` holds, then there exists `x` in `α` with frequency in `f` having both `p(x)` and `q(x)`.
|
Filter.le_seq
theorem Filter.le_seq :
∀ {α : Type u} {β : Type v} {f : Filter (α → β)} {g : Filter α} {h : Filter β},
(∀ t ∈ f, ∀ u ∈ g, t.seq u ∈ h) → h ≤ f.seq g
The theorem `Filter.le_seq` states that for any three filters `f`, `g`, and `h` over functions from type `α` to type `β`, type `α`, and type `β` respectively, if for every set `t` in the filter `f` and every set `u` in the filter `g`, the sequentiation of `t` and `u` (which is the union of the image of `t` by all functions in `u`) belongs to filter `h`, then filter `h` is a subset of the sequentiation of filters `f` and `g`. Here, subset is defined in the sense of filters, i.e., `h` is a subset of `f` if every set in `h` is also in `f`.
More concisely: If for all sets $T \in f$ and $U \in g$, the sequentiation of $T$ and $U$ is contained in $h$, then $f$ and $g$ filter-contain $h$, i.e., every set in $h$ is also in the filter generated by $f$ and $g$.
|
Filter.nonempty_of_neBot
theorem Filter.nonempty_of_neBot : ∀ {α : Type u} (f : Filter α) [inst : f.NeBot], Nonempty α
This theorem states that for any type `α` and any filter `f` over this type, if the filter `f` is not the bottom filter (which intuitively means it's not "empty"), then the type `α` is nonempty. In other words, if we have some nontrivial filter on a type, then there must exist at least one element of that type.
More concisely: If a filter over a type is non-bottom, then the type is nonempty.
|
Filter.Tendsto.neBot
theorem Filter.Tendsto.neBot :
∀ {α : Type u} {β : Type v} {f : α → β} {x : Filter α} {y : Filter β},
Filter.Tendsto f x y → ∀ [hx : x.NeBot], y.NeBot
The theorem `Filter.Tendsto.neBot` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any filters `x` on `α` and `y` on `β`, if `f` tends to transform `x` into `y` (i.e., `Filter.Tendsto f x y`), and if `x` is a filter that is not the bottom filter (i.e., `Filter.NeBot x`), then `y` must also be a filter that is not the bottom filter (i.e., `Filter.NeBot y`). In mathematical terms, if a function has a limit within a non-empty neighborhood, the limit itself is also in a non-empty neighborhood.
More concisely: If a function transforms a non-bottom filter into a limit, then the limit is a non-bottom filter.
|
Filter.EventuallyLE.biUnion
theorem Filter.EventuallyLE.biUnion :
∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
s.Finite →
∀ {f g : ι → Set α}, (∀ i ∈ s, l.EventuallyLE (f i) (g i)) → l.EventuallyLE (⋃ i ∈ s, f i) (⋃ i ∈ s, g i)
This theorem, known as `Filter.EventuallyLE.biUnion`, states the following: given a type `α`, a filter `l` on `α`, a type `ι`, and a set `s` of type `ι`, if `s` is finite, and for every `i` in `s`, `l` is eventually less than or equal to both `f i` and `g i` (where `f` and `g` are functions from `ι` to the set of `α`), then `l` is also eventually less than or equal to the union of `f i` and `g i` for each `i` in `s`. In other words, if a filter is eventually less than or equal to each of a finite collection of sets, it is also eventually less than or equal to their union.
More concisely: Given a filter `l` on a type `α`, a finite set `s` of indexes, and functions `f` and `g` from `s` to `α`, if `l` is eventually less than or equal to both `f i` and `g i` for all `i` in `s`, then `l` is eventually less than or equal to the union of `{fi | i ∈ s}` and `{gi | i ∈ s}`.
|
Filter.EventuallyEq.fun_comp
theorem Filter.EventuallyEq.fun_comp :
∀ {α : Type u} {β : Type v} {γ : Type w} {f g : α → β} {l : Filter α},
l.EventuallyEq f g → ∀ (h : β → γ), l.EventuallyEq (h ∘ f) (h ∘ g)
This theorem states that for any types `α`, `β`, and `γ`, and for any functions `f` and `g` from `α` to `β` and a function `h` from `β` to `γ`, if `f` and `g` are eventually equal at a filter `l` on `α`, then the compositions `h ∘ f` and `h ∘ g` will also be eventually equal at the same filter `l`. In mathematical notation, this is saying that if $f =_l g$, then $h \circ f =_l h \circ g$.
More concisely: If functions $f : \alpha \to \beta$ and $g : \alpha \to \beta$ have equal values at a filter $l$ on $\alpha$, then the compositions $h \circ f$ and $h \circ g$ have equal values at the same filter $l$, for any function $h : \beta \to \gamma$.
|
Filter.tendsto_congr'
theorem Filter.tendsto_congr' :
∀ {α : Type u} {β : Type v} {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β},
l₁.EventuallyEq f₁ f₂ → (Filter.Tendsto f₁ l₁ l₂ ↔ Filter.Tendsto f₂ l₁ l₂)
The theorem `Filter.tendsto_congr'` states that for any two functions `f₁` and `f₂` from a type `α` to another type `β`, and any two filters `l₁` on `α` and `l₂` on `β`, if `f₁` is eventually equal to `f₂` at `l₁` (denoted by `f₁ =ᶠ[l₁] f₂`), then `f₁` tends to `l₂` along `l₁` if and only if `f₂` also tends to `l₂` along `l₁`. Here, "tends to `l₂` along `l₁`" means that for every neighborhood `a` of `l₂`, the preimage of `a` under the function is a neighborhood of `l₁`.
More concisely: For functions `f₁` and `f₂` from type `α` to type `β`, and filters `l₁` on `α` and `l₂` on `β`, if `f₁` is eventually equal to `f₂` at `l₁` and for every neighborhood `a` of `l₂`, the preimage of `a` under `f₁` is a neighborhood of `l₁` if and only if the same holds for `f₂`, then `f₁` and `f₂` both tend to `l₂` along `l₁`.
|
Filter.mem_iInf_of_directed
theorem Filter.mem_iInf_of_directed :
∀ {α : Type u} {ι : Sort x} {f : ι → Filter α},
Directed (fun x x_1 => x ≥ x_1) f → ∀ [inst : Nonempty ι] (s : Set α), s ∈ iInf f ↔ ∃ i, s ∈ f i
The theorem `Filter.mem_iInf_of_directed` states that for all types `α` and `ι`, and a function `f` mapping `ι` to a filter on `α`, if the function `f` is directed with respect to the greater than or equal to relation (meaning, for any two filters in the image of `f`, there is a filter which is greater than or equal to both), then for any nonempty `ι` and a set `s` of type `α`, the set `s` is a member of the infimum of the range of `f` if and only if there exists an `i` such that `s` is a member of the filter `f i`.
In simpler terms, it states that a set `s` is in the infimum of a directed family of filters if and only if `s` is in one of the filters in the family.
More concisely: Given a type `α`, a nonempty index type `ι`, and a directed family `{F : ι → filter α | i ∈ ι}`, a set `s ∈ α` belongs to the infimum of the family if and only if there exists an index `i` such that `s ∈ F i`.
|
Mathlib.Order.Filter.Basic._auxLemma.83
theorem Mathlib.Order.Filter.Basic._auxLemma.83 :
∀ {α : Type u} {a : Set α} {p : α → Prop}, (∀ᶠ (x : α) in Filter.principal a, p x) = ∀ x ∈ a, p x
This theorem states that for any type `α`, any set `a` of type `α`, and any predicate `p` acting on `α`, the statement "for all `x` in `α` eventually in the filter generated by the principal set `a`, `p` holds" is equivalent to "for all `x` in the set `a`, `p` holds". In simpler words, this theorem relates properties that hold eventually in a filter generated by a set (i.e., on all elements in the set and possibly more) to properties that hold on all elements in the set itself.
More concisely: The theorem asserts that for any type `α`, set `a` of `α`, and predicate `p` on `α`, the filter generated by `a` eventually includes all elements of `α` satisfying `p` if and only if all elements of `a` satisfy `p`.
|
Filter.Eventually.mono
theorem Filter.Eventually.mono :
∀ {α : Type u} {p q : α → Prop} {f : Filter α},
(∀ᶠ (x : α) in f, p x) → (∀ (x : α), p x → q x) → ∀ᶠ (x : α) in f, q x
This theorem, `Filter.Eventually.mono`, states that for any type `α`, any two properties `p` and `q` of `α`, and any filter `f` of `α`, if `p` holds eventually at `f` and `p` implies `q` for all `α`, then `q` also holds eventually at `f`. In mathematical terms, given $f$ is a filter on a type $\alpha$ and $p$ and $q$ are propositions about elements of $\alpha$, if for all elements in $f$, $p$ holds eventually, and if for all elements of $\alpha$, $p$ implies $q$, then for all elements in $f$, $q$ also holds eventually.
More concisely: If `p` holds eventually in a filter `f` of type `α` and `p` implies `q` for all `α`, then `q` holds eventually in `f`. (Mathematically: For all filters `f` on a type `α` and propositions `p` and `q` on `α`, if `p` holds eventually in `f` and `p` implies `q` for all `α`, then `q` holds eventually in `f`. )
|
Filter.EventuallyEq.inter
theorem Filter.EventuallyEq.inter :
∀ {α : Type u} {s t s' t' : Set α} {l : Filter α},
l.EventuallyEq s t → l.EventuallyEq s' t' → l.EventuallyEq (s ∩ s') (t ∩ t')
The theorem `Filter.EventuallyEq.inter` states that for any type `α`, sets `s`, `t`, `s'`, `t'` of type `α` and a filter `l` on `α`, if `s` is eventually equal to `t` under the filter `l` and `s'` is eventually equal to `t'` under the same filter, then the intersection of `s` and `s'` is eventually equal to the intersection of `t` and `t'` under the filter `l`. Here, the term "eventually equal" refers to the idea that for all elements beyond a certain point in the filtered set, the property holds.
More concisely: If filters `l` make sets `s` and `t` eventually equal, and sets `s'` and `t'` similarly, then the intersections of `s` and `s'` and `t` and `t'` are eventually equal under filter `l`.
|
Mathlib.Order.Filter.Basic._auxLemma.14
theorem Mathlib.Order.Filter.Basic._auxLemma.14 : ∀ {α : Type u} {f : Filter α} {s : Set α}, (s ∈ f) = (s ∈ f.sets)
This theorem, named as `Mathlib.Order.Filter.Basic._auxLemma.14`, states that for any type `α`, any filter `f` on `α`, and any set `s` of elements of type `α`, the proposition that `s` belongs to `f` is equivalent to the proposition that `s` belongs to the collection of sets in `f`. In other words, a set is a member of a given filter if and only if it is a member of the collection of sets that constitute that filter.
More concisely: For any filter `f` on type `α` and any set `s` of elements of type `α`, `s` belongs to filter `f` if and only if there exists a set `t` in `f` such that `s` is a subset of `t`.
|
Filter.comap_map
theorem Filter.comap_map :
∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β},
Function.Injective m → Filter.comap m (Filter.map m f) = f
This theorem states that for all types `α` and `β`, for any filter `f` on the type `α`, and for any injective function `m` from `α` to `β`, the composition of the comap of `m` and the map of `m` applied to `f` is equal to `f` itself. In simpler terms, it says that if you first map a filter `f` from `α` to `β` using an injective function and then comap it back to `α` using the same function, you end up with the original filter `f`. This is similar to the mathematical concept that the composition of a function and its inverse results in the identity function, in this case, the filter remains unchanged.
More concisely: For all filters $f$ on type $\alpha$, and for any injective function $m:\alpha \rightarrow \beta$, the composition of $m \circ \map(m)(f)$ equals $f$.
|
Filter.Tendsto.comp
theorem Filter.Tendsto.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {x : Filter α} {y : Filter β} {z : Filter γ},
Filter.Tendsto g y z → Filter.Tendsto f x y → Filter.Tendsto (g ∘ f) x z
The theorem `Filter.Tendsto.comp` asserts that for all types `α`, `β`, and `γ`, and for all functions `f : α → β` and `g : β → γ`, and all filters `x : Filter α`, `y : Filter β` and `z : Filter γ`, if function `g` tends towards filter `z` when starting from filter `y`, and function `f` tends towards filter `y` when started from filter `x`, then the composition of `g` and `f` (i.e., `g ∘ f`) also tends towards `z` when started from `x`. This theorem essentially establishes the property of composition for the limit of a function in the context of filters.
More concisely: If functions `f : α → β` and `g : β → γ` tend towards filters `z : Filter γ` and `y : Filter β`, respectively, when started from filters `x : Filter α` and `y`, then the composition `g ∘ f` tends towards `z` when started from `x`.
|
HasSubset.Subset.eventuallyLE
theorem HasSubset.Subset.eventuallyLE : ∀ {α : Type u_1} {l : Filter α} {s t : Set α}, s ⊆ t → l.EventuallyLE s t := by
sorry
This theorem states that for any type `α`, any filter `l` on `α`, and any two sets `s` and `t` of `α`, if `s` is a subset of `t`, then `s` is eventually less than or equal to `t` with respect to the filter `l`. Here, "eventually less than or equal to" is denoted by `≤ᶠ[l]` and represents a concept from the theory of filters in topology.
More concisely: For any filter `l` on type `α`, if `s` is a subset of `t` in `α`, then `s ≤ᶠ[l] t` holds.
|
Filter.eventually_all_finset
theorem Filter.eventually_all_finset :
∀ {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ι → α → Prop},
(∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
This theorem establishes an equivalence relation for all elements in a finite set `I` of type `ι` and a filter `l` of type `α`. It asserts that for any predicate `p` which takes an element from `I` and an element from `l` to produce a proposition, it is equivalent to say that 'eventually' (for all elements beyond a certain point) in the filter `l`, for all elements `i` in the finite set `I`, the proposition `p i x` holds true AND to say that for all elements `i` in the finite set `I`, 'eventually' in the filter `l`, the proposition `p i x` holds true. Here, 'eventually' refers to the concept in filter theory that describes a condition that holds for all elements outside some finite subset.
More concisely: For a finite set `I` and a filter `l` on a type `α`, the relation that for all `i ∈ I` and `x ∈ l`, `p i x` holds eventually in `l` if and only if for all `i ∈ I`, `p i x` holds eventually in `l` for some `x`, is an equivalence relation.
|
Filter.tendsto_iff_comap
theorem Filter.tendsto_iff_comap :
∀ {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
Filter.Tendsto f l₁ l₂ ↔ l₁ ≤ Filter.comap f l₂
The theorem `Filter.tendsto_iff_comap` states that for any types `α` and `β`, 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 `l₁` is less than or equal to the preimage filter of `f` along `l₂`. In other words, for all `α`, `β`, `f`, `l₁`, and `l₂`, the function `f` has the limit of `l₂` at `l₁` if and only if every set in `l₁` contains the preimage under `f` of some set in `l₂`.
More concisely: For types `α` and `β`, functions `f` from `α` to `β`, and filters `l₁` on `α` and `l₂` on `β`, the function `f` tends to `l₂` along `l₁` if and only if `l₁` is contained in the preimage filter of `f` along `l₂`.
|
Filter.eventually_sub_nonneg
theorem Filter.eventually_sub_nonneg :
∀ {α : Type u} {β : Type v} [inst : OrderedRing β] {l : Filter α} {f g : α → β},
l.EventuallyLE 0 (g - f) ↔ l.EventuallyLE f g
The theorem `Filter.eventually_sub_nonneg` states that for any two functions `f` and `g` from a type `α` to an ordered ring `β` and any filter `l` on `α`, the difference `g - f` is nonnegative eventually (at some point and for all points thereafter) with respect to filter `l` if and only if `f` is lesser than or equal to `g` eventually with respect to the same filter. The direction of implication goes both ways: if the difference is nonnegative, then `f` is less than or equal to `g`, and vice versa.
More concisely: For any functions $f, g : \alpha \to \beta$ from a type $\alpha$ to an ordered ring $\beta$, and any filter $l$ on $\alpha$, the difference $g - f$ is eventually nonnegative with respect to $l$ if and only if $f$ is eventually less than or equal to $g$ with respect to $l$.
|
Filter.tendsto_bot
theorem Filter.tendsto_bot : ∀ {α : Type u} {β : Type v} {f : α → β} {l : Filter β}, Filter.Tendsto f ⊥ l
The theorem `Filter.tendsto_bot` states that for any types `α` and `β`, any function `f` from `α` to `β`, and any filter `l` on `β`, the function `f` tends from the bottom filter of `α` to `l`. In other words, for every neighborhood `a` of `l` in `β`, the preimage under `f` of `a` is a neighborhood in the bottom filter of `α`. This theorem is a specific instance of the general concept of a function tending towards a certain limit, where the limit is defined via filters.
More concisely: For any functions `f: α -> β`, `l: Filter β`, and neighborhood `a` of `l` in `β`, the preimage `f ^^-1 (a)` is a neighborhood in the bottom filter of `α`.
|
Filter.univ_mem
theorem Filter.univ_mem : ∀ {α : Type u} {f : Filter α}, Set.univ ∈ f
The theorem `Filter.univ_mem` asserts that for any type `α` and any filter `f` on `α`, the universal set of `α` is an element of `f`. In other words, it states that the universal set, which contains all elements of a given type, is part of any filter defined on that type. In set theoretic terms, if we consider `f` as a collection of subsets of `α`, this theorem is equivalent to stating that the whole set `α` is one of those subsets.
More concisely: For any type `α` and filter `f` on `α`, the universal set of `α` belongs to `f`.
|
Mathlib.Order.Filter.Basic._auxLemma.79
theorem Mathlib.Order.Filter.Basic._auxLemma.79 :
∀ {α : Type u} {p : α → Prop}, (∀ᶠ (x : α) in ⊤, p x) = ∀ (x : α), p x
This theorem states that for any type `α` and a property `p` that applies to elements of `α`, the statement "for almost every `x` of type `α` in the top filter, `p x` holds" is equivalent to "for every `x` of type `α`, `p x` holds". Here, the top filter (represented by `⊤`) is a filter that contains all subsets of `α`. Thus, the theorem establishes that in such a universal context, the concepts of "almost every" and "every" coincide.
More concisely: For any type `α` and property `p` on `α`, "p holds for almost every x in α if and only if p holds for all x in α" (equivalently, "p holds for almost all x in the top filter on α if and only if p holds universally on α").
|
Filter.mem_map
theorem Filter.mem_map :
∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {t : Set β}, t ∈ Filter.map m f ↔ m ⁻¹' t ∈ f
The theorem `Filter.mem_map` states that for any types `α` and `β`, any filter `f` over `α`, any function `m` from `α` to `β`, and any set `t` of `β`, the set `t` is in the filter produced by mapping `f` through `m` if and only if the preimage of `t` under `m` is in `f`. This essentially means that applying the function `m` to the filter `f` and then checking for the presence of the set `t` is equivalent to first applying the function `m` to the set `t` to get its preimage, and then checking if this preimage is in the filter `f`.
More concisely: For any filter `f` on type `α`, function `m` from `α` to `β`, and set `t` of `β`, `t ∈ map f m` if and only if `m⁻¹("t") ∈ f`.
|
Filter.EventuallyEq.biUnion
theorem Filter.EventuallyEq.biUnion :
∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
s.Finite →
∀ {f g : ι → Set α}, (∀ i ∈ s, l.EventuallyEq (f i) (g i)) → l.EventuallyEq (⋃ i ∈ s, f i) (⋃ i ∈ s, g i)
This theorem, an alias of `Set.Finite.eventuallyEq_iUnion`, states that for any type `α`, any filter `l` on `α`, any type `ι`, and any finite set `s` of type `ι`, if two functions `f` and `g` from `ι` to the set of `α` are eventually equal at each element of `s` under the filter `l`, then the unions of `f i` and `g i` over all `i` in `s` are also eventually equal under filter `l`.
In other words, if `f i` and `g i` are eventually the same for each index in our finite set, then the unions of these sets will also be eventually the same. This theorem connects the concept of eventual equality (in the context of filters) with operations on indexed unions over finite sets.
More concisely: For any type `α`, filter `l` on `α`, type `ι`, and finite set `s` of `ι`, if functions `f` and `g` from `ι` to `α` are eventually equal at each index in `s` under filter `l`, then the unions of `f i` and `g i` over all `i` in `s` are eventually equal under filter `l`.
|
Mathlib.Order.Filter.Basic._auxLemma.30
theorem Mathlib.Order.Filter.Basic._auxLemma.30 :
∀ {α : Type u} {ι : Sort x} {x : Set α} {f : ι → Filter α}, (x ∈ iSup f) = ∀ (i : ι), x ∈ f i
This theorem establishes a property of the indexed supremum of a collection of filters. Specifically, it states that for any type `α`, any indexing set `ι`, any set `x` of type `α`, and any function `f` from `ι` to `Filter α`, the set `x` is in the indexed supremum of the collection `f` if and only if `x` is in every filter of that collection. In other words, the set `x` belongs to the supremum of the filters indexed by `ι` (i.e., `iSup f`) exactly when for each index `i` in `ι`, `x` is an element of the filter `f(i)`.
More concisely: For any type `α`, indexing set `ι`, set `x` of type `α`, and function `f` from `ι` to `Filter α`, `x` belongs to the indexed supremum `iSup f` if and only if it is an element of every filter `f(i)` in the collection.
|
Filter.forall_mem_nonempty_iff_neBot
theorem Filter.forall_mem_nonempty_iff_neBot : ∀ {α : Type u} {f : Filter α}, (∀ s ∈ f, s.Nonempty) ↔ f.NeBot := by
sorry
This theorem states that for any type 'α' and any filter 'f' on that type, the filter 'f' is not the bottom filter (`Filter.NeBot f`) if and only if every set 's' in the filter 'f' is not empty (`∀ s ∈ f, Set.Nonempty s`). Here, a bottom filter refers to the smallest filter in the filter lattice structure that contains all filters, analogous to the role of zero in a number system. The 'Set.Nonempty s' property indicates that there exists at least one element in the set 's'.
More concisely: A filter on a type is not the bottom filter if and only if it contains only non-empty sets.
|
Filter.map_swap_eq_comap_swap
theorem Filter.map_swap_eq_comap_swap :
∀ {α : Type u} {β : Type v} {f : Filter (α × β)}, Prod.swap <$> f = Filter.comap Prod.swap f
The theorem `Filter.map_swap_eq_comap_swap` states that for all types `α` and `β`, and for any filter `f` of pairs from `α` and `β`, mapping the `Prod.swap` function over the filter `f` is equivalent to the co-domain (comap) of the `Prod.swap` function with respect to the filter `f`. In simpler terms, it's saying the operation of swapping elements in each pair in the filter is the same whether we do it in the domain (using map) or in the co-domain (using comap).
More concisely: For any filter on pairs from types `α` and `β`, mapping `Prod.swap` is equivalent to composing `Prod.swap` with the filter's comap operation.
|
Mathlib.Order.Filter.Basic._auxLemma.134
theorem Mathlib.Order.Filter.Basic._auxLemma.134 : ∀ {α : Type u} {a : α} {s : Set α}, ({a} ⊆ s) = (a ∈ s)
This theorem states that for any type `α`, any element `a` of type `α`, and any set `s` of type `α`, the singleton set containing `a` is a subset of `s` if and only if `a` is an element of `s`. In other words, a singleton set `{a}` is included in another set `s` precisely when the element `a` is in `s`.
More concisely: For any type `α`, set `s` of type `α`, and element `a` of type `α`, the singleton set `{a}` is a subset of `s` if and only if `a` is an element of `s`. (Equivalently, `a` belongs to `s` if and only if the singleton set `{a}` is a subset of `s`.)
|
Filter.le_map
theorem Filter.le_map :
∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {g : Filter β}, (∀ s ∈ f, m '' s ∈ g) → g ≤ Filter.map m f
This theorem, named `Filter.le_map`, states that for every types `α` and `β`, every filter `f` on `α`, every function `m` from `α` to `β`, and every filter `g` on `β`, if for every set `s` in the filter `f`, the image of `s` under `m` is in the filter `g`, then `g` is less than or equal to the filter obtained by forward mapping the filter `f` using `m`. In other words, if all the images of the sets in `f` under `m` are in `g`, then `g` includes all the sets that could possibly be obtained by applying `m` to the sets in `f`.
More concisely: If a filter `f` on `α` maps to a filter `g` on `β` via a function `m` such that every set in `f` maps to a set in `g`, then `g` is less than or equal to the filter obtained by applying `m` to `f`.
|
Filter.ext_iff
theorem Filter.ext_iff : ∀ {α : Type u} {f g : Filter α}, f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
The theorem `Filter.ext_iff` states the following: for any type `α` and any two filters `f` and `g` over `α`, `f` is equal to `g` if and only if for every set `s` of type `α`, `s` is in `f` if and only if `s` is in `g`. In other words, two filters are considered equal if they contain exactly the same sets.
More concisely: Two filters over a type `α` are equal if and only if they contain the same sets.
|
Filter.Eventually.exists
theorem Filter.Eventually.exists :
∀ {α : Type u} {p : α → Prop} {f : Filter α} [inst : f.NeBot], (∀ᶠ (x : α) in f, p x) → ∃ x, p x
This theorem states that for any type `α`, any predicate `p` that applies to elements of `α`, and any filter `f` of `α` which is not a bottom filter (i.e., it is not the filter that includes all sets), if `p` holds eventually (i.e., in all sufficiently large elements) for `f`, then there exists an element `x` for which `p` holds. In terms of mathematical terminology, if we have `∀ᶠ (x : α) in f, p x`, which means `p` is true for all `x` outside of a set in the filter `f` of negligibly small measure, then there exists an `x` such that `p(x)` is true.
More concisely: If a predicate `p` holds eventually in a filter `f` of a type `α` that is not the bottom filter, then there exists an element `x` in `α` belonging to `f` such that `p(x)` is true.
|
Filter.mem_principal
theorem Filter.mem_principal : ∀ {α : Type u} {s t : Set α}, s ∈ Filter.principal t ↔ t ⊆ s
This theorem states that, for any type `α` and any two sets `s` and `t` of this type, `s` is in the principal filter of `t` if and only if `t` is a subset of `s`. In the context of filters in mathematics, the "principal filter of `t`" is the collection of all sets which contain `t`. Therefore, this theorem is saying that a set `s` is in this collection exactly when `t` is included in `s`.
More concisely: A set `s` is the principal filter of set `t` if and only if `t` is a subset of `s`.
|
Filter.eventually_principal
theorem Filter.eventually_principal :
∀ {α : Type u} {a : Set α} {p : α → Prop}, (∀ᶠ (x : α) in Filter.principal a, p x) ↔ ∀ x ∈ a, p x
This theorem, `Filter.eventually_principal`, states that for any type `α`, any set `a` of type `α`, and any property `p`, a statement of the form "eventually, for every element `x` in the principal filter of `a`, `p x` holds" is equivalent to the statement "for every `x` in `a`, `p x` holds". In other words, a property `p` holds eventually for all elements in the principal filter of a set `a` if and only if the property holds for all elements in the set `a` itself.
More concisely: The theorem asserts that for any set `a` and property `p`, the property holds eventually for all elements in the principal filter of `a` if and only if it holds for all elements in `a`.
|
Filter.mp_mem
theorem Filter.mp_mem : ∀ {α : Type u} {f : Filter α} {s t : Set α}, s ∈ f → {x | x ∈ s → x ∈ t} ∈ f → t ∈ f
The theorem `Filter.mp_mem` states that for any type `α`, any filter `f` on `α`, and any two sets `s` and `t` of type `α`, if `s` is in `f` and all elements of `s` are also in `t`, then `t` is in `f`. Here, "being in `f`" is interpreted as the set being in the collection defined by the filter `f`. This theorem is a form of modus ponens specialized to the context of filters and sets.
More concisely: If a filter `f` on a type `α` contains a set `s`, and every element of `s` is in another set `t`, then `t` is contained in `f`.
|
Filter.iInf_sets_eq_finite
theorem Filter.iInf_sets_eq_finite :
∀ {α : Type u} {ι : Type u_2} (f : ι → Filter α), (⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i).sets
This theorem states that for any given type `α` and another type `ι`, and a function `f` from `ι` to `Filter α`, the intersection of the sets generated by the function `f` applied across all of `ι` is equal to the union of the sets generated by the function `f` applied across each finite subset `t` of `ι`. In the context of filters, this result ties together the concept of intersection (represented by `⨅`) and union (represented by `⋃`), showing how they relate when applied to all elements versus finite subsets.
More concisely: For any type `α` and type `ι`, and a function `f` from `ι` to filters on `α`, the intersection of images `⨅ i ∈ ι. f i` equals the union of images `⋃ t ⊆ ι. {⨅ j ∈ t. f j}`.
|
Filter.comap_principal
theorem Filter.comap_principal :
∀ {α : Type u} {β : Type v} {m : α → β} {t : Set β},
Filter.comap m (Filter.principal t) = Filter.principal (m ⁻¹' t)
This theorem states that given two types `α` and `β`, a function `m` from `α` to `β`, and a set `t` of elements of type `β`, the preimage filter of the function `m` when applied to the principal filter of the set `t` is equal to the principal filter of the preimage of the set `t` under the function `m`. In other words, it establishes a relationship between the operation of filter preimage and the principal filter construction on sets. The preimage of a set under a function is the set of all elements that map to any element of the original set, and a principal filter of a set is the collection of all supersets of that set.
More concisely: Given functions between sets and principal filters, the preimage filter of a function applied to a principal filter is equal to the principal filter of the preimage of the set under the function.
|
Filter.Tendsto.congr'
theorem Filter.Tendsto.congr' :
∀ {α : Type u} {β : Type v} {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β},
l₁.EventuallyEq f₁ f₂ → Filter.Tendsto f₁ l₁ l₂ → Filter.Tendsto f₂ l₁ l₂
The theorem `Filter.Tendsto.congr'` establishes the congruence of `Filter.Tendsto`, a predicate which represents the limit of a function. Specifically, for any two functions `f₁` and `f₂` from type `α` to type `β`, and any two filters `l₁` on type `α` and `l₂` on type `β`, if `f₁` and `f₂` are eventually equal at `l₁` (denoted as `f₁ =ᶠ[l₁] f₂`), and if `f₁` tends to `l₂` along `l₁` (represented by `Filter.Tendsto f₁ l₁ l₂`), then `f₂` also tends to `l₂` along `l₁` (expressed as `Filter.Tendsto f₂ l₁ l₂`). In other words, the limit of a function at a point is unaffected if we change the function at a set of points that has negligible "size" in the context of the considered filter.
More concisely: If `f₁` and `f₂` are eventually equal at a filter `l₁` and `f₁` tends to a filter `l₂` along `l₁`, then `f₂` also tends to `l₂` along `l₁`.
|
Set.EqOn.eventuallyEq
theorem Set.EqOn.eventuallyEq :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f g : α → β}, Set.EqOn f g s → (Filter.principal s).EventuallyEq f g
This theorem states that for any two functions `f` and `g` from some type `α` to another type `β`, and a set `s` of elements from `α`, if these two functions are equal on the set `s` (that is, `f(x) = g(x)` for every `x` in `s`), then `f` is almost everywhere equal to `g` on the principal filter of `s`. The principal filter of a set is the collection of all supersets of that set. In other words, except possibly on a subset of `s` of negligible size, `f` and `g` have the same values.
More concisely: If functions `f` and `g` from type `α` to type `β` agree on set `s`, then they are almost equal on the principal filter of `s`, i.e., agree outside a subset of negligible size.
|
Finset.iInter_mem_sets
theorem Finset.iInter_mem_sets :
∀ {α : Type u} {f : Filter α} {β : Type v} {s : β → Set α} (is : Finset β), ⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
The theorem `Finset.iInter_mem_sets` states that for any types `α` and `β`, any filter `f` of type `Filter α`, and any function `s` from `β` to `Set α`, and a finite set `is` of type `Finset β`, the intersection over sets `s i` for all `i` in the finite set `is` belongs to the filter `f` if and only if each set `s i` for every `i` in `is` belongs to the filter `f`. In mathematical terms, this theorem is stating that for a filter `f` and a collection of sets `s i` indexed by elements in a finite set, the intersection of all `s i` is in `f` if and only if each `s i` is in `f`.
More concisely: For any filter `f` on type `α`, and any function `s` from type `β` to sets of `α`, a finite set `is` of indices from `β`, the intersection of the sets `s i` for all `i` in `is` is in `f` if and only if each set `s i` is in `f`.
|
Filter.ext'
theorem Filter.ext' :
∀ {α : Type u} {f₁ f₂ : Filter α}, (∀ (p : α → Prop), (∀ᶠ (x : α) in f₁, p x) ↔ ∀ᶠ (x : α) in f₂, p x) → f₁ = f₂
This theorem states that for any two filters `f₁` and `f₂` of a given type `α`, if for any predicate `p` of type `α → Prop`, the property `p` holds eventually (denoted by `∀ᶠ`) in `f₁` if and only if it holds eventually in `f₂`, then `f₁` and `f₂` are equal. In simple terms, two filters are equal if every predicate that eventually holds true in one filter also eventually holds true in the other filter, and vice versa.
More concisely: Two filters `f₁` and `f₂` over type `α` are equal if and only if they have the same eventualities for all predicates `p` of type `α → Prop`.
|
Filter.Eventually.and
theorem Filter.Eventually.and :
∀ {α : Type u} {p q : α → Prop} {f : Filter α},
Filter.Eventually p f → Filter.Eventually q f → ∀ᶠ (x : α) in f, p x ∧ q x
The theorem `Filter.Eventually.and` states that for any type `α`, any two properties `p` and `q` of `α`, and any filter `f` of `α`, if `p` holds eventually in `f` (meaning the set of `α` for which `p` is true belongs to `f`) and `q` also holds eventually in `f`, then there exists a point in the filter `f` beyond which both `p` and `q` hold true. In other words, it is saying that the conjunction of two properties (both `p` and `q` being true) also holds eventually in the filter `f`.
More concisely: If filters `f` contain sets of elements on which properties `p` and `q` hold eventually, then there exists an element in `f` where both `p` and `q` hold true.
|
Filter.univ_sets
theorem Filter.univ_sets : ∀ {α : Type u_1} (self : Filter α), Set.univ ∈ self.sets
The theorem `Filter.univ_sets` asserts that for any type `α` and any filter on that type (represented by `self : Filter α`), the universal set of `α` (denoted by `Set.univ`) is an element of the set of sets included in the filter. In other words, the universal set belongs to every filter. This is analogous to the set-theoretic concept that the universal set is a subset of every set.
More concisely: For any filter `self` on type `α`, the universal set `Set.univ` of `α` is an element of `self`.
|
Filter.mem_sets
theorem Filter.mem_sets : ∀ {α : Type u} {f : Filter α} {s : Set α}, s ∈ f.sets ↔ s ∈ f
This theorem states that for any type `α`, any filter `f` of type `α`, and any set `s` of type `α`, the set `s` is a member of the sets of the filter `f` if and only if `s` is a member of the filter `f`. That is, the membership of a set in the sets of a filter is equivalent to the membership of the set in the filter itself.
More concisely: For any filter `f` on type `α`, a set `s` belongs to the sets in `f` if and only if `s` belongs to `f`.
|
Filter.inter_sets
theorem Filter.inter_sets :
∀ {α : Type u_1} (self : Filter α) {x y : Set α}, x ∈ self.sets → y ∈ self.sets → x ∩ y ∈ self.sets
This theorem states that for any type `α` and a filter on `α` (represented as `self`), if there are two sets `x` and `y` of type `α` that belong to the collections of sets (named `self.sets`) of this filter, then their intersection (represented as `x ∩ y`) also belongs to `self.sets`. In other words, if two sets are in the filter, their intersection is also in the filter. This theorem generalizes one of the fundamental properties of filters in set theory.
More concisely: If `α` is a type and `self` is a filter on `α`, then for all `x, y ∈ self.sets`, we have `x ∩ y ∈ self.sets`.
|
Filter.map_comap
theorem Filter.map_comap :
∀ {α : Type u} {β : Type v} (f : Filter β) (m : α → β),
Filter.map m (Filter.comap m f) = f ⊓ Filter.principal (Set.range m)
This theorem states that for any types `α` and `β`, a filter `f` on `β`, and a map `m` from `α` to `β`, the filter obtained by first taking the inverse image of `f` under `m` (using `Filter.comap m f`) and then taking the direct image under `m` (using `Filter.map m`) is equal to the filter obtained by taking the intersection of `f` and the filter consisting of all supersets of the range of `m` (using `Filter.principal (Set.range m)`). In other words, mapping the comap of a filter under a function is the same as intersecting the original filter with the principal filter of the range of that function. In terms of set theory, this theorem is expressing a property about the interaction of inverse and direct image filters under a function and how it relates to the intersection of filters.
More concisely: For any map $m:\alpha \to \beta$, filter $f$ on $\beta$, and type $\alpha$, the filters $m.\mathit{inverseImage} (f)$ and $f \cap \mathit{principalFilter} (\mathrm{range} (m))$ are equal.
|
Filter.Tendsto.mono_right
theorem Filter.Tendsto.mono_right :
∀ {α : Type u} {β : Type v} {f : α → β} {x : Filter α} {y z : Filter β},
Filter.Tendsto f x y → y ≤ z → Filter.Tendsto f x z
The theorem `Filter.Tendsto.mono_right` states that for all types `α` and `β`, for any function `f` from `α` to `β`, and for any filters `x` on `α` and `y` and `z` on `β`, if the function `f` tends towards the filter `y` under the filter `x`, and if the filter `y` is a subset of the filter `z`, then the function `f` also tends towards the filter `z` under the filter `x`. In other words, if `f` maps every neighborhood of `x` to a neighborhood of `y`, and `y` is contained in `z`, then `f` maps every neighborhood of `x` to a neighborhood of `z`.
More concisely: If a function tends towards a filter under another filter, and the smaller filter is a subset of a larger filter, then the function also tends towards the larger filter under the same domain filter.
|
Filter.Tendsto.mono_left
theorem Filter.Tendsto.mono_left :
∀ {α : Type u} {β : Type v} {f : α → β} {x y : Filter α} {z : Filter β},
Filter.Tendsto f x z → y ≤ x → Filter.Tendsto f y z
The theorem `Filter.Tendsto.mono_left` states that for all types `α` and `β`, for all functions `f` mapping from `α` to `β`, and for all filters `x`, `y` on `α` and a filter `z` on `β`, if `f` tends to filter `z` via filter `x`, and filter `y` is less or equal to filter `x`, then `f` also tends to filter `z` via filter `y`. In other words, it states that if `f` is converging with respect to a larger filter, it also converges with respect to any of its smaller subfilters.
More concisely: If `f` tends to filter `z` via filter `x`, and `x` is a subset of `y`, then `f` tends to filter `z` via filter `y`.
|
Filter.tendsto_map'
theorem Filter.tendsto_map' :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ},
Filter.Tendsto (f ∘ g) x y → Filter.Tendsto f (Filter.map g x) y
This theorem, named `Filter.tendsto_map'`, states that for any types `α`, `β`, and `γ`, and any functions `f : β → γ` and `g : α → β`, along with any filters `x : Filter α` and `y : Filter γ`, if the function composed of `f` and `g` (i.e., `(f ∘ g)`) tends from filter `x` to filter `y`, then the function `f` tends from the filter mapped by `g` over `x` to filter `y`. In other words, if `(f ∘ g)` has a limit at some point in the context of filters `x` and `y`, then `f` also has a limit at that point in the context of the filters obtained by applying `g` to `x` and the original filter `y`.
More concisely: If `f : β → γ` tends to a limit in `Filter.tendsto y (f ∘ g)` for filters `x : Filter α` and `y : Filter γ`, then `f` also tends to a limit in `Filter.tendsto (g ^-1 '[] y) f`, where `g : α → β`.
|
Filter.principal_univ
theorem Filter.principal_univ : ∀ {α : Type u}, Filter.principal Set.univ = ⊤
The theorem `Filter.principal_univ` states that for any type `α`, the principal filter of the universal set `Set.univ` (which includes all elements of type `α`) is equal to the top filter (often denoted as `⊤`). In other words, the collection of all supersets of the universal set for any given type is the same as the most inclusive filter, or top filter.
More concisely: The principal filter of the universal set in any type equals the top filter.
|
Filter.iInf_principal_finset
theorem Filter.iInf_principal_finset :
∀ {α : Type u} {ι : Type w} (s : Finset ι) (f : ι → Set α),
⨅ i ∈ s, Filter.principal (f i) = Filter.principal (⋂ i ∈ s, f i)
This theorem states that for every finite set `s` of elements of some type `ι` and a function `f` from `ι` to sets of elements of type `α`, the infimum (greatest lower bound) of the principal filters of the images of the elements in `s` under `f` is equal to the principal filter of the intersection of the images of the elements in `s` under `f`. In other words, the principal filter of the intersection of a collection of sets is equal to the infimum of the principal filters of the sets in the collection, when the collection is a finite set.
More concisely: For every finite set `s` and function `f` from a type `ι` to sets of type `α`, the infimum of the principal filters of `f` applied to elements in `s` equals the principal filter of the intersection of `f`'s images on `s`.
|
Filter.eventually_const
theorem Filter.eventually_const : ∀ {α : Type u} {f : Filter α} [t : f.NeBot] {p : Prop}, (∀ᶠ (x : α) in f, p) ↔ p := by
sorry
This theorem, `Filter.eventually_const`, states that for any type `α` and a filter `f` of `α` that is not a bottom filter (i.e., it is not the empty set), given a proposition `p`, the proposition `p` is eventually true for every element in the filter `f` if and only if `p` is true. This means that if `p` is true, then there exists a point beyond which all elements of the filter satisfy `p`, and conversely, if there exists a point beyond which all elements of the filter satisfy `p`, then `p` is true.
More concisely: For any filter `f` on type `α` that is not bottom and proposition `p`, `p` is eventually true for all elements in `f` if and only if `p` holds.
|
Filter.tendsto_const_pure
theorem Filter.tendsto_const_pure :
∀ {α : Type u} {β : Type v} {a : Filter α} {b : β}, Filter.Tendsto (fun x => b) a (pure b)
The theorem `Filter.tendsto_const_pure` states that for all types `α` and `β`, given a filter `a` on the type `α`, and an element `b` of type `β`, the constant function that maps every element of `α` to `b` tends to the pure filter at `b` under the filter `a`. In other words, for every neighborhood of `b` in the codomain, its preimage under the constant function is a neighborhood of `a` in the domain.
More concisely: For any filter `a` on type `α` and any element `b` of type `β`, the constant function from `α` to `β` maps `a` to the pure filter at `b`.
|
Mathlib.Order.Filter.Basic._auxLemma.2
theorem Mathlib.Order.Filter.Basic._auxLemma.2 : ∀ {α : Type u} {f : Filter α} {s : Set α}, (s ∈ f.sets) = (s ∈ f) := by
sorry
The theorem "`Mathlib.Order.Filter.Basic._auxLemma.2`" states that for any type `α`, any filter `f` of type `α`, and any set `s` of type `α`, the predicate that `s` is in the set of `f`'s sets (written as `s ∈ f.sets`) is equivalent to the predicate that `s` is in `f` (written as `s ∈ f`). In other words, the two ways of expressing set membership in a filter are equivalent.
More concisely: For any filter `f` on type `α`, the set `f.sets` contains a set `s` if and only if `s` is in the filter `f`. That is, `s ∈ f.sets` if and only if `s ∈ f`.
|
Mathlib.Order.Filter.Basic._auxLemma.132
theorem Mathlib.Order.Filter.Basic._auxLemma.132 : ∀ {α : Type u} {a : α} {s : Set α}, (s ∈ pure a) = (a ∈ s) := by
sorry
This theorem states that for any type `α`, any element `a` of type `α`, and any set `s` of elements of type `α`, the property that set `s` belongs to the filter generated by `a` (represented as `pure a`) is equivalent to the property that `a` belongs to the set `s`. In the context of filters in order theory, `pure a` represents the principal filter generated by `a`, which consists of all sets that contain `a`. Therefore, the theorem is establishing a fundamental property of principal filters.
More concisely: For any type `α`, element `a` of type `α`, and set `s` of elements of type `α`, the set `s` belongs to the filter generated by `a` if and only if `a` is an element of `s`.
|
Mathlib.Order.Filter.Basic._auxLemma.117
theorem Mathlib.Order.Filter.Basic._auxLemma.117 :
∀ {α : Type u} {s t : Set α} {l : Filter α},
l.EventuallyLE s t = (l ⊓ Filter.principal s ≤ l ⊓ Filter.principal t)
This theorem states that for any type `α`, any two sets `s` and `t` of this type, and any filter `l` on this type, the condition that set `s` is lesser than or equal to set `t` in the filter order of `l` is equivalent to the condition that the infimum (or greatest lower bound) of the filter `l` and the principal filter of `s` is lesser than or equal to the infimum of the filter `l` and the principal filter of `t`. Here, the principal filter of a set is the collection of all supersets of that set. The filter order `≤ᶠ[l]` refers to the order of sets in the context of the filter `l`, where one set is considered less than or equal to another if it contains the other.
More concisely: For any type `α`, filter `l` on `α`, sets `s` and `t` of `α`, the condition `s ≤ᶠ[l] t` if and only if `inf(l, filter.principal s) ≤ inf(l, filter.principal t)`.
|
Mathlib.Order.Filter.Basic._auxLemma.80
theorem Mathlib.Order.Filter.Basic._auxLemma.80 :
∀ {α : Type u} {p : α → Prop} {f g : Filter α},
(∀ᶠ (x : α) in f ⊔ g, p x) = ((∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in g, p x)
This theorem states that, for any type `α` and any predicate `p` on `α`, along with any two filters `f` and `g` on `α`, the property `p` holding eventually (meaning in the filter) in the sup (join or union) of `f` and `g` is equivalent to `p` holding eventually in both `f` and `g`. In mathematical terms, for all $x$ of type $α$, $p(x)$ holds eventually in the sup of the two filters if and only if $p(x)$ holds eventually in each of the filters separately.
More concisely: For any type `α`, predicate `p` on `α`, and filters `f` and `g` on `α`, `p` eventually holds in the sup of `f` and `g` if and only if `p` eventually holds in both `f` and `g`.
|
Filter.EventuallyEq.biInter
theorem Filter.EventuallyEq.biInter :
∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
s.Finite →
∀ {f g : ι → Set α}, (∀ i ∈ s, l.EventuallyEq (f i) (g i)) → l.EventuallyEq (⋂ i ∈ s, f i) (⋂ i ∈ s, g i)
The theorem `Filter.EventuallyEq.biInter` states that for any types `α` and `ι`, any filter `l` on `α`, any finite set `s` of `ι`, and any two functions `f` and `g` from `ι` to the sets of `α`, if each set `f i` is eventually equal to `g i` at all `i` belonging to `s` with respect to the filter `l`, then the intersection of all sets `f i` for `i` in `s` is eventually equal to the intersection of all sets `g i` for `i` in `s` with respect to the same filter `l`.
In other words, if every set in a certain collection defined by `f` eventually equals the corresponding set defined by `g` under a given filter, then the intersection of all sets in the `f`-defined collection will eventually equal the intersection of all sets in the `g`-defined collection under the same filter, provided that the set of indices defining the collections is finite.
More concisely: If filters `l` on type `α`, functions `f` and `g` from a finite set `ι` to `α`, and for all `i` in `ι`, `Filter.EventuallyEq.eventually_eq l i f i g i`, then `∩ (fi : Set α) i in s = ∩ (gi : Set α) i in s`.
|
Filter.comap_bot
theorem Filter.comap_bot : ∀ {α : Type u} {β : Type v} {m : α → β}, Filter.comap m ⊥ = ⊥
This theorem states that for any types `α` and `β`, and any function `m` mapping from `α` to `β`, the preimage filter of the bottom filter (the filter containing only the empty set) under the function `m` is also the bottom filter. In other words, when you take the preimage of the empty set through any function, you always get the empty set.
More concisely: For any function `m` between types `α` and `β`, the preimage of the bottom filter under `m` is the bottom filter.
|
Mathlib.Order.Filter.Basic._auxLemma.169
theorem Mathlib.Order.Filter.Basic._auxLemma.169 :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ},
Filter.Tendsto f (Filter.map g x) y = Filter.Tendsto (f ∘ g) x y
This theorem asserts that for all types `α`, `β`, and `γ`, and for all functions `f : β → γ`, `g : α → β`, and given two filters `x : Filter α` and `y : Filter γ`, the statement that `f` tends to `y` under the filter that arises from mapping `g` over `x` (expressed as `Filter.Tendsto f (Filter.map g x) y`) is equivalent to the statement that the composition of `f` and `g` tends to `y` under the filter `x` (expressed as `Filter.Tendsto (f ∘ g) x y`). In other words, the "limit" behavior of the composed function `(f ∘ g)` under a filter is the same as applying `f` to the "limit" of `g` under the same filter. This theorem is a formal statement of the limit of a composition of functions in the context of filters.
More concisely: The theorem states that for all types `α`, `β`, `γ`, functions `f : β → γ`, `g : α → β`, and filters `x : Filter α` and `y : Filter γ`, the filter convergence `Filter.Tendsto f (Filter.map g x) y` is equivalent to `Filter.Tendsto (f ∘ g) x y`.
|
Mathlib.Order.Filter.Basic._auxLemma.51
theorem Mathlib.Order.Filter.Basic._auxLemma.51 : ∀ {a b c : Prop}, (a ∧ b → c) = (a → b → c)
This theorem states that for any three propositions `a`, `b`, and `c`, the proposition "`a` and `b` implies `c`" is logically equivalent to the proposition "if `a` then `b` implies `c`". Essentially, it encapsulates the fact that we can rephrase a statement involving a conjunction (an "and" statement) and an implication (a "then" statement) as a statement involving nested implications, without changing the truth of the statement.
More concisely: The theorem asserts that `(a ∧ b) → c` is logically equivalent to `a → (b → c)`.
|
Filter.eventually_sup
theorem Filter.eventually_sup :
∀ {α : Type u} {p : α → Prop} {f g : Filter α},
(∀ᶠ (x : α) in f ⊔ g, p x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in g, p x
This theorem states that for all types `α` and any predicate `p` on `α`, along with any two filters `f` and `g` on `α`, a proposition `p` is eventually true in the supremum (`⊔`) of filters `f` and `g` if and only if `p` is eventually true in both filters `f` and `g`. In mathematical language, it can be said that a property holds eventually in the supremum of two filters if and only if it holds eventually in both of the original filters.
More concisely: For all types `α` and predicates `p` on `α`, if `p` is eventually true in both filters `f` and `g` on `α`, then `p` is eventually true in their supremum `f ⊔ g`.
|
Filter.tendsto_comap
theorem Filter.tendsto_comap :
∀ {α : Type u} {β : Type v} {f : α → β} {x : Filter β}, Filter.Tendsto f (Filter.comap f x) x
The theorem `Filter.tendsto_comap` states that for all types `α` and `β`, for all functions from `α` to `β` denoted as `f`, and for all filters on `β` denoted as `x`, the function `f` tends to the filter `x` when composed with the preimage under `f` of filter `x`. In simple terms, applying `f` to the preimages of the elements of `x` under `f` will map us back into the neighborhood of `x`. This confirms that the function `f` respects the filter structure and it's a fundamental property in filter theory.
More concisely: For any type `α` and function `f` from `α` to `β`, and filter `x` on `β`, if `f` tends to `x`, then the preimage `f⁁⁻¹(x)` under `f` also tends to `x`.
|
Filter.image_mem_map
theorem Filter.image_mem_map :
∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {s : Set α}, s ∈ f → m '' s ∈ Filter.map m f
This theorem states that for any types `α` and `β`, any filter `f` on `α`, any function `m` from `α` to `β`, and any set `s` of type `α`, if `s` is a member of the filter `f`, then the image of `s` under the function `m` is a member of the filter obtained by applying the map function on `m` and `f`. In mathematical terms, if `s` is in the filter `f`, then the image of `s` under `m` is in the forward map of `f` under `m`.
More concisely: If `f` is a filter on type `α`, `m` is a function from `α` to `β`, and `s` is a subset of `α` that belongs to `f`, then the image of `s` under `m` belongs to the filter obtained by applying the map function to `m` and `f`.
|
Filter.inter_mem_inf
theorem Filter.inter_mem_inf : ∀ {α : Type u} {f g : Filter α} {s t : Set α}, s ∈ f → t ∈ g → s ∩ t ∈ f ⊓ g
The theorem `Filter.inter_mem_inf` states that for any given type `α`, and any given filters `f` and `g` over this type, if a set `s` is in filter `f` and another set `t` is in filter `g`, then the intersection of sets `s` and `t` is in the infimum (greatest lower bound) of filters `f` and `g`. In other words, the intersection of any two sets each belonging to different filters also belongs to the filter which is the infimum of the original two filters.
More concisely: If filters $f$ and $g$ over type $\alpha$ have a common lower bound, then the intersection of any sets in $f$ and any sets in $g$ is in this lower bound.
|
Filter.mem_sup
theorem Filter.mem_sup : ∀ {α : Type u} {f g : Filter α} {s : Set α}, s ∈ f ⊔ g ↔ s ∈ f ∧ s ∈ g
This theorem, named `Filter.mem_sup`, is about filters and sets in a general context where `α` denotes any Type. It states that for every type `α`, every pair of filters `f` and `g` on `α`, and every set `s` of elements of type `α`, the set `s` is in the supremum (defined as `f ⊔ g`) of the filters `f` and `g` if and only if `s` is in both the filter `f` and the filter `g`. In simpler words, a set is in the union of two filters if and only if it is in both filters.
More concisely: For all types `α`, filters `f` and `g` on `α`, and sets `s` of elements of type `α`, `s ∈ f ⊔ g` if and only if `s ∈ f` and `s ∈ g`.
|
Filter.le_principal_iff
theorem Filter.le_principal_iff : ∀ {α : Type u} {s : Set α} {f : Filter α}, f ≤ Filter.principal s ↔ s ∈ f
The theorem `Filter.le_principal_iff` establishes a relationship between filters and sets in a certain type `α`. For any type `α`, any set `s` of type `α`, and any filter `f` on `α`, the theorem states that the filter `f` is less than or equal to the principal filter of `s` if and only if `s` is an element of the filter `f`. In other words, it provides a condition on the relationship between a filter and a set such that the filter being a subset of all supersets of a given set is equivalent to the set being in the filter.
More concisely: A filter `f` on a type `α` is equal to the principal filter of a set `s` if and only if `s` is an element of `f`.
|
Filter.EventuallyEq.refl
theorem Filter.EventuallyEq.refl : ∀ {α : Type u} {β : Type v} (l : Filter α) (f : α → β), l.EventuallyEq f f := by
sorry
This theorem states that, for any type `α` and `β`, and any filter `l` of type `α` and a function `f` from `α` to `β`, the function `f` is eventually equal to itself with respect to the filter `l`. "Eventually equal" is a concept in analysis meaning that the two functions are equal except possibly on a set of measure zero (or more generally, on a set that the filter does not "see").
More concisely: For any type `α`, filter `l` on `α`, and function `f` from `α` to `β`, there exists a set in `l` on which `f` is equal to its restriction to that set.
|
Filter.preimage_mem_comap
theorem Filter.preimage_mem_comap :
∀ {α : Type u} {β : Type v} {g : Filter β} {m : α → β} {t : Set β}, t ∈ g → m ⁻¹' t ∈ Filter.comap m g
This theorem states that for all types `α` and `β`, a filter `g` on `β`, a function `m` from `α` to `β`, and a set `t` of type `β`, if `t` is in `g`, then the preimage of `t` under `m` is in the comap of `m` and `g`. Here, the preimage of `t` under `m` is the set of all elements in `α` that `m` maps to `t`, and the comap of `m` and `g` is the filter on `α` consisting of all preimages of sets in `g` under `m`.
More concisely: For all types `α` and `β`, filters `g` on `β`, functions `m` from `α` to `β`, and sets `t` in `g`, the preimage of `t` under `m` belongs to the composite filter of `m` and `g`.
|
Filter.map_neBot_iff
theorem Filter.map_neBot_iff :
∀ {α : Type u} {β : Type v} (f : α → β) {F : Filter α}, (Filter.map f F).NeBot ↔ F.NeBot
The theorem `Filter.map_neBot_iff` states that for any types `α` and `β`, a function `f` from `α` to `β`, and a filter `F` on `α`, the forward image filter `Filter.map f F` under the function `f` is non-trivial (i.e., doesn't contain only the empty set) if and only if the original filter `F` is non-trivial. This means that the non-triviality of a filter is preserved under the operation of taking forward images.
More concisely: For any functions f between types α and β and filters F on α, the filter obtained by applying the function f to the elements of F (Filter.map f F) is non-empty if and only if the original filter F is non-empty.
|
Mathlib.Order.Filter.Basic._auxLemma.176
theorem Mathlib.Order.Filter.Basic._auxLemma.176 :
∀ {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {x : ι → Filter α} {y : Filter β},
Filter.Tendsto f (⨆ i, x i) y = ∀ (i : ι), Filter.Tendsto f (x i) y
The theorem `Mathlib.Order.Filter.Basic._auxLemma.176` states that for any types `α` and `β`, any sort `ι`, any function `f` from `α` to `β`, any function `x` from `ι` to the set of filters on `α`, and any filter `y` on `β`, the function `f` tends to the filter `y` under the join (supremum) of the filters `x i` (for each `i` in `ι`) if and only if for each `i` in `ι`, the function `f` tends to the filter `y` under the filter `x i`. In other words, the limit of `f` at the supremum of the filters is the same as the limit of `f` at each of the individual filters.
More concisely: For any types α and β, functions f from α to β, filters x on α indexed by an index set ι, and a filter y on β, the function f tends to the filter y under the join of x i (for each i in ι) if and only if for all i in ι, the function f tends to the filter y under the filter x i.
|
Filter.inter_mem
theorem Filter.inter_mem : ∀ {α : Type u} {f : Filter α} {s t : Set α}, s ∈ f → t ∈ f → s ∩ t ∈ f
The theorem `Filter.inter_mem` states that for any type `α`, any filter `f` on `α`, and any two sets `s` and `t` of type `α`, if both `s` and `t` are in `f`, then their intersection `s ∩ t` is also in `f`. In other words, the intersection of two sets belonging to a filter is also a member of the same filter.
More concisely: If `f` is a filter on type `α`, and `s` and `t` are both elements of `f`, then their intersection `s ∩ t` is also an element of `f`.
|
Filter.Tendsto.frequently
theorem Filter.Tendsto.frequently :
∀ {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop},
Filter.Tendsto f l₁ l₂ → (∃ᶠ (x : α) in l₁, p (f x)) → ∃ᶠ (y : β) in l₂, p y
The theorem `Filter.Tendsto.frequently` asserts that if a function `f` defined from one type `α` to another type `β` tends to a limit `l₂` at a point `l₁`, and if there frequently exists an `x` in the filter `l₁` such that a certain property `p` holds for `f(x)`, then there frequently exists a `y` in the filter `l₂` for which the property `p` also holds. Here, "frequently" means that the statement holds on a set that is not a "small" neighborhood of `l₁` or `l₂`, respectively, and "tends to a limit `l₂` at a point `l₁`" means that for any neighborhood of `l₂`, its inverse image under `f` is a neighborhood of `l₁`.
More concisely: If a function `f` tends to a limit `l₂` at `l₁` and there is a filter on `l₁` such that the property `p` holds for `f(x)` frequently in that filter, then there is a filter on `l₂` such that `p` holds for `f(y)` frequently in that filter.
|
Filter.map_inf
theorem Filter.map_inf :
∀ {α : Type u} {β : Type v} {f g : Filter α} {m : α → β},
Function.Injective m → Filter.map m (f ⊓ g) = Filter.map m f ⊓ Filter.map m g
This theorem, named `Filter.map_inf`, states that for any types `α` and `β`, any two filters `f` and `g` on `α`, and any function `m` from `α` to `β` that is injective, the map of the intersection of `f` and `g` under `m` is equivalent to the intersection of the map of `f` under `m` and the map of `g` under `m`. In other words, if `m` is a function that doesn't map different elements to the same value (it's injective), then mapping the intersection of two filters through `m` is the same as intersecting the individual mappings of the two filters.
More concisely: For injective functions `m` from type `α` to type `β`, the map of the intersection of filters `f` and `g` on `α` under `m` equals the intersection of the maps of `f` and `g` under `m`.
|
Filter.mem_inf_of_inter
theorem Filter.mem_inf_of_inter :
∀ {α : Type u} {f g : Filter α} {s t u : Set α}, s ∈ f → t ∈ g → s ∩ t ⊆ u → u ∈ f ⊓ g
This theorem states that for any type `α`, given two filters `f` and `g` over `α`, and three sets `s`, `t`, and `u` of elements of type `α`, if `s` is in the filter `f`, `t` is in the filter `g`, and the intersection of sets `s` and `t` is a subset of `u`, then `u` is in the infimum (i.e., the greatest lower bound) of the filters `f` and `g`. In other words, `u` is a member of the filter which is the intersection of `f` and `g`.
More concisely: Given filters `f` and `g` over type `α`, if `s` in `f`, `t` in `g`, and `s ∩ t ⊆ u`, then `u` is in the infimum of `f` and `g`.
|
Filter.EventuallyEq.rfl
theorem Filter.EventuallyEq.rfl : ∀ {α : Type u} {β : Type v} {l : Filter α} {f : α → β}, l.EventuallyEq f f
The Lean theorem `Filter.EventuallyEq.rfl` states that, for any type `α` and `β`, any filter `l` on type `α`, and any function `f` from `α` to `β`, `f` is eventually equal to itself with respect to the filter `l`. In other words, at some point and thereafter, every value f(x) equals f(x). This theorem is a reflection of the reflexivity property in the context of filters and functions.
More concisely: For any filter `l` on type `α` and function `f` from `α` to `β`, there exists an index `n` such that for all `i ≥ n`, `f(l.at i) = f(l.at i)`. Here, `l.at i` represents the element in `α` that `l` selects at index `i`.
|
Mathlib.Order.Filter.Basic._auxLemma.12
theorem Mathlib.Order.Filter.Basic._auxLemma.12 : ∀ {α : Type u} {s t : Set α}, (s ∈ Filter.principal t) = (t ⊆ s) := by
sorry
This theorem states that for any type `α` and any two sets `s` and `t` of type `α`, `s` is in the principal filter of `t` if and only if `t` is a subset of `s`. In other words, `s` is a member of all supersets of `t` (which is what the principal filter of `t` represents) if and only if every element of `t` is also an element of `s`.
More concisely: For any type `α` and sets `s` and `t` of type `α`, `s` is the principal filter of `t` if and only if `t` is a subset of `s`.
|
Filter.map_eq_comap_of_inverse
theorem Filter.map_eq_comap_of_inverse :
∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {n : β → α},
m ∘ n = id → n ∘ m = id → Filter.map m f = Filter.comap n f
The theorem `Filter.map_eq_comap_of_inverse` states that for any types `α` and `β`, any filter `f` on `α`, and any functions `m` from `α` to `β` and `n` from `β` to `α`, if `m` composed with `n` equals the identity function and `n` composed with `m` also equals the identity function, then the forward map of `f` through `m` is equal to the co-filter of `f` through `n`. Essentially, this theorem is about the symmetry between forward mapping and co-filtering in the context of filters when there exist inverse functions between the types.
More concisely: Given filters `f` on type `α`, functions `m: α → β` and `n: β → α` such that `m ∘ n = id_β` and `n ∘ m = id_α`, then `Filter.map f m = Filter.comap f n`.
|
Filter.EventuallyEq.comp₂
theorem Filter.EventuallyEq.comp₂ :
∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} {f f' : α → β} {g g' : α → γ} {l : Filter α},
l.EventuallyEq f f' →
∀ (h : β → γ → δ), l.EventuallyEq g g' → l.EventuallyEq (fun x => h (f x) (g x)) fun x => h (f' x) (g' x)
This theorem, `Filter.EventuallyEq.comp₂`, is about function composition and equality with respect to a filter. It states that for all types `α`, `β`, `γ`, and `δ`, and all functions `f`, `f'`, `g`, `g'` from `α` to `β` and `α` to `γ` respectively, and a filter `l` on `α`, if `f` is eventually equal to `f'` at filter `l`, and `g` is also eventually equal to `g'` at the same filter `l`, then the function which takes two arguments and applies `h` to `f` of the first and `g` of the second is eventually equal to the function which applies `h` to `f'` of the first and `g'` of the second at filter `l`. Essentially, this tells us about the preservation of eventual equality under the composition of binary functions.
More concisely: Given filters `l` on types `α`, functions `f : α -> β`, `f' : α -> β`, `g : α -> γ`, and `g' : α -> γ`, if `f` is eventually equal to `f'` at filter `l`, and `g` is eventually equal to `g'` at filter `l`, then the composition `h . (f &&& g)` is eventually equal to `h . (f' &&& g')` at filter `l`, for any function `h : β -> γ`.
|
Mathlib.Order.Filter.Basic._auxLemma.168
theorem Mathlib.Order.Filter.Basic._auxLemma.168 :
∀ {α : Type u} {β : Type v} {f : α → β} {l : Filter α}, Filter.Tendsto f l ⊤ = True
This theorem states that for any types `α` and `β`, any function `f` from `α` to `β`, and any filter `l` on `α`, the condition that `f` tends to `l` at the top filter (denoted as `⊤`) is always true. In other words, for any function and any filter, the image of the filter under the function is always a subset of the top filter. The top filter is a special filter that contains all sets, so this theorem is saying that the image of any filter under any function is always a valid filter.
More concisely: For any function between types and any filter, the image of the filter under the function is a subset of the top filter.
|
Mathlib.Order.Filter.Basic._auxLemma.97
theorem Mathlib.Order.Filter.Basic._auxLemma.97 :
∀ {α : Type u} {f : Filter α} {p q : α → Prop},
(∃ᶠ (x : α) in f, p x ∨ q x) = ((∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in f, q x)
This theorem states that for any type `α`, any filter `f` of `α`, and any two predicate functions `p` and `q` on `α`, the eventuality that `p` or `q` holds for some element in `f` is equivalent to the eventuality that `p` holds for some element in `f` or `q` holds for some element in `f`. The notation `∃ᶠ (x : α) in f, p x` is used to represent the eventuality (in the filter `f`) that the predicate `p` is true for some `α`.
More concisely: For any filter `f` on type `α` and any predicate functions `p` and `q` on `α`, the eventualities `∃ᶠ (x : α) in f, p x` and `∃ᶠ (x : α) in f, p x ∨ q x` are equivalent.
|
Filter.comap_mono
theorem Filter.comap_mono : ∀ {α : Type u} {β : Type v} {m : α → β}, Monotone (Filter.comap m)
The theorem `Filter.comap_mono` states that for all types `α` and `β`, and for all functions `m` from `α` to `β`, the function `Filter.comap m` is monotone. This means for any given function `m`, if `a` and `b` are elements of type `α` such that `a ≤ b`, then the result of `Filter.comap m` applied to `a` is less than or equal to the result of `Filter.comap m` applied to `b`. In other words, `Filter.comap` preserves the order of elements under the function `m`.
More concisely: For all types α and β, and for all functions m from α to β, the monotone function Filter.comap m preserves the order, that is, a ≤ b implies Filter.m a ≤ Filter.m b.
|
Filter.eventuallyEq_iff_exists_mem
theorem Filter.eventuallyEq_iff_exists_mem :
∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β}, l.EventuallyEq f g ↔ ∃ s ∈ l, Set.EqOn f g s
The theorem `Filter.eventuallyEq_iff_exists_mem` states that for any types `α` and `β`, any filter `l` on `α`, and any functions `f` and `g` from `α` to `β`, the assertion that `f` is eventually equal to `g` at filter `l` (denoted `f =ᶠ[l] g`) is equivalent to the existence of a set `s` which belongs to the filter `l` such that `f` and `g` are equal on `s`. In other words, `f` is eventually equal to `g` at `l` if and only if there is some set `s` in the filter `l` where `f` and `g` have the same values for all elements of `s`.
More concisely: For any types `α` and `β`, filter `l` on `α`, and functions `f` and `g` from `α` to `β`, `f` is eventually equal to `g` at filter `l` if and only if there exists a set `s` in `l`, such that `f(x) = g(x)` for all `x` in `s`.
|
Filter.comap_sup
theorem Filter.comap_sup :
∀ {α : Type u} {β : Type v} {g₁ g₂ : Filter β} {m : α → β},
Filter.comap m (g₁ ⊔ g₂) = Filter.comap m g₁ ⊔ Filter.comap m g₂
This theorem states that for any two filters `g₁` and `g₂` on a type `β` and any function `m` from a type `α` to `β`, the filter derived by mapping the sup (greatest lower bound) of `g₁` and `g₂` back to `α` through `m` is the same as the sup of the filters derived by mapping `g₁` and `g₂` separately back to `α`. In other words, the operation of "pulling back" a filter through a function commutes with taking the sup of two filters. This is a fundamental property in the theory of filters in mathematics.
More concisely: For filters $g\_1$ and $g\_2$ on type $\beta$, and a function $m:\alpha \to \beta$, the pullback of the supremum of $g\_1$ and $g\_2$ through $m$ equals the supremum of the pullbacks of $g\_1$ and $g\_2$ through $m$.
|
Filter.tendsto_map'_iff
theorem Filter.tendsto_map'_iff :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : β → γ} {g : α → β} {x : Filter α} {y : Filter γ},
Filter.Tendsto f (Filter.map g x) y ↔ Filter.Tendsto (f ∘ g) x y
The theorem `Filter.tendsto_map'_iff` states that for any types `α`, `β`, and `γ`, and any functions `f : β → γ` and `g : α → β`, and any filters `x : Filter α` and `y : Filter γ`, the function `f` has the limit `y` after applying the forward map `g` on the filter `x` if and only if the function `f` composed with `g` has the limit `y` on the filter `x`. In other words, mapping a filter and then taking a limit is the same as composing the functions and then taking a limit.
More concisely: For filters $x : Filter(\alpha)$, $y : Filter(\gamma)$, functions $f : \beta \rightarrow \gamma$, and $g : \alpha \rightarrow \beta$, $f$ has the limit $y$ after mapping $x$ if and only if $f \circ g$ has the limit $y$ on $x$.
|
Filter.Iic_principal
theorem Filter.Iic_principal : ∀ {α : Type u} (s : Set α), Set.Iic (Filter.principal s) = {l | s ∈ l}
This theorem states that for any set `s` of a certain type `α`, the left-infinite right-closed interval of the principal filter of `s` is equivalent to the set of all sets `l` that contain `s`. In other words, when we take the principal filter of a set `s` (which is the collection of all supersets of `s`) and apply the operation `Set.Iic` (which represents a left-infinite right-closed interval), we end up with the set of all sets `l` where `s` is a member.
More concisely: The principal filter of a set `s` equals the set of all sets containing `s` up to right-closed intervals.
|
Filter.Eventually.mp
theorem Filter.Eventually.mp :
∀ {α : Type u} {p q : α → Prop} {f : Filter α},
(∀ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, p x → q x) → ∀ᶠ (x : α) in f, q x
The theorem `Filter.Eventually.mp` states that for any type `α`, any properties `p` and `q` of `α`, and any filter `f` on `α`, if `p` holds eventually for some `x` in the filter `f`, and if it is also the case that `p x` implies `q x` eventually in the filter `f`, then `q` also holds eventually for some `x` in the filter `f`. In other words, it shows that the "eventually" filter condition is closed under logical implication.
More concisely: If a property `p` holds eventually for some elements in a filter `f` and `p(x)` implies `q(x)` eventually in `f` for all `x` in the domain, then property `q` holds eventually for some elements in the filter `f`.
|
Mathlib.Order.Filter.Basic._auxLemma.66
theorem Mathlib.Order.Filter.Basic._auxLemma.66 :
∀ {α : Type u} {f : Filter α} {s t : Set α}, (s ∈ f ⊓ Filter.principal t) = ({x | x ∈ t → x ∈ s} ∈ f)
This theorem, named `Mathlib.Order.Filter.Basic._auxLemma.66`, states that for any given type `α`, any filter `f` on that type, and any two sets `s` and `t` of that type, the condition that `s` is in the intersection of `f` and the principal filter of `t` is equivalent to the condition that the set of elements `x` which are in `s` whenever they are in `t` is in the filter `f`. In simpler terms, it's saying that `s` being in the intersection of `f` and the filter of all supersets of `t` is the same as `f` containing all elements that are in `s` given that they are in `t`.
More concisely: For any type `α`, filter `f` on `α`, and sets `s` and `t` in `α`, `s` is in the intersection of `f` and the principal filter of `t` if and only if the set of elements in `s` that are also in `t` is in `f`.
|
Filter.map_pure
theorem Filter.map_pure : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α), Filter.map f (pure a) = pure (f a) := by
sorry
The theorem `Filter.map_pure` states that for any types `α` and `β`, and a function `f` from `α` to `β`, the forward map of a filter applied to the function `f` and the pure filter generated by an element `a` of `α` is equal to the pure filter generated by `f(a)`. Simply put, mapping a function over a pure filter just applies the function to the element in the pure filter.
More concisely: For any type `α`, type `β`, and function `f : α → β`, the application of a filter to `f` and the pure filter generated by an element `a ∈ α` results in the same filter as the pure filter generated by `f(a)`. In mathematical notation: `Filter.map f (pure a) = pure (f a)`.
|
Filter.iInter_mem
theorem Filter.iInter_mem :
∀ {α : Type u} {f : Filter α} {β : Sort v} {s : β → Set α} [inst : Finite β], ⋂ i, s i ∈ f ↔ ∀ (i : β), s i ∈ f
This theorem states that for any type `α`, any filter `f` of type `Filter α`, and any function `s` mapping from type `β` to the set of `α`, given that `β` is finite, the intersection over all `i` of `s i` is in `f` if and only if for all `i` in `β`, `s i` is in `f`. In simpler terms, it's telling us that the condition of all sets `s i` being in a given filter `f` is equivalent to the intersection of all such sets being in filter `f`.
More concisely: For any filter `f` on type `α`, any finite type `β`, and function `s` from `β` to `α`, if for all `i` in `β`, `s i` is in `f`, then the intersection of `s i` for all `i` is in `f`. Conversely, if the intersection of `s i` is in `f`, then each `s i` is in `f`.
|
Filter.eventually_all_finite
theorem Filter.eventually_all_finite :
∀ {α : Type u} {ι : Type u_2} {I : Set ι},
I.Finite →
∀ {l : Filter α} {p : ι → α → Prop}, (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
The theorem `Filter.eventually_all_finite` states that for all types `α` and `ι`, and for a finite set `I` of type `ι`, any filter `l` of type `α`, and a property `p` that takes a type `ι` and a type `α` to a proposition, the proposition that "for almost all `x` in the filter `l`, for all `i` in the set `I`, `p i x` holds" is equivalent to the proposition that "for all `i` in the set `I`, for almost all `x` in the filter `l`, `p i x` holds". In other words, the order of quantifiers does not matter when the set `I` is finite.
More concisely: For any filter `l` over type `α`, property `p` taking `ι` and `α` to props, and finite set `I` of type `ι`, the statements "for almost all `x` in `l`, for all `i` in `I`, `p i x` holds" and "for all `i` in `I`, for almost all `x` in `l`, `p i x` holds" are equivalent.
|
Filter.comap_iInf
theorem Filter.comap_iInf :
∀ {α : Type u} {β : Type v} {ι : Sort x} {m : α → β} {f : ι → Filter β},
Filter.comap m (⨅ i, f i) = ⨅ i, Filter.comap m (f i)
This theorem states that for any types `α` and `β`, any indexed type `ι`, any function `m` from `α` to `β`, and any function `f` from `ι` to the set of filters on `β`, the filter obtained by applying the `comap` operation to `m` and the infimum of the filters `f i` (for all `i` in `ι`) is equal to the infimum of the filters obtained by applying `comap` to `m` and `f i` (for all `i` in `ι`). In mathematical terms, this can be written as `comap(m, ⨅ i, f i) = ⨅ i, comap(m, f i)`.
More concisely: For any functions `m: α → β` and `f: ι → Filters β`, the filter `comap(m) ��asm ap f` equals the infimum of `comap(m) ��asm ap (fi)` for all `i` in `ι`.
|
Filter.eventually_pure
theorem Filter.eventually_pure : ∀ {α : Type u} {a : α} {p : α → Prop}, (∀ᶠ (x : α) in pure a, p x) ↔ p a
This theorem, `Filter.eventually_pure`, states that for any type `α`, any element `a` of that type, and any property `p` applicable to elements of type `α`, the proposition "eventually for all `x` in the pure filter of `a`, property `p` holds for `x`" is equivalent to the proposition "property `p` holds for `a`". In simpler terms, it says that if a property holds eventually for all elements in a pure filter on `a`, it must hold for `a` itself, and vice versa. A pure filter in this context is a filter that contains only `a` and sets that include `a`.
More concisely: For any type `α`, element `a` of type `α`, and property `p` applicable to `α`, `a` belongs to the eventual filter of `p` if and only if `p` holds for `a`.
|
Filter.tendsto_iInf'
theorem Filter.tendsto_iInf' :
∀ {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {x : ι → Filter α} {y : Filter β} (i : ι),
Filter.Tendsto f (x i) y → Filter.Tendsto f (⨅ i, x i) y
The theorem `Filter.tendsto_iInf'` states that for any types `α` and `β`, sorting type `ι`, a function `f` from `α` to `β`, a family of filters `x` indexed by `ι` on `α`, and a filter `y` on `β`, given an index `i` in `ι`, if the function `f` tends to the filter `y` when applied to the filter `x i`, then `f` also tends to `y` when applied to the infimum of the family of filters `x`. In essence, it asserts that if a function converges to a limit under a particular filter in a family, it also converges to that same limit under the infimum of the entire family of filters.
More concisely: If a function converges pointwise to a filter on its codomain with respect to a family of filters on its domain, then it converges to the same filter under the infimum of the family.
|
Filter.map_comap_le
theorem Filter.map_comap_le :
∀ {α : Type u} {β : Type v} {g : Filter β} {m : α → β}, Filter.map m (Filter.comap m g) ≤ g
The theorem `Filter.map_comap_le` states that for any types `α` and `β`, any filter `g` on `β`, and any function `m` from `α` to `β`, the map of the filter obtained by first co-mapping `g` through `m` and then mapping it through `m` is less than or equal to `g`. In other words, if we first pull `g` back through `m` and then push it forward again, we will get a filter that's a "subset" of (or equal to) our original filter `g`. It represents a fundamental property of filters related to function mappings.
More concisely: For any filter \(g\) on type \(\beta\), function \(m : \alpha \to \beta\), and \(F : \Set (\Subset \beta)\), \(F = \downarrow\!\circ m \circ g \uparrow \iff F \subseteq g\).
In other words, the filter obtained by first lifting \(g\) through \(m\) and then pushing it back down is a subset of \(g\).
|
Filter.singleton_mem_pure
theorem Filter.singleton_mem_pure : ∀ {α : Type u} {a : α}, {a} ∈ pure a
This theorem, named `Filter.singleton_mem_pure`, states that for any type `α` and any element `a` of type `α`, the singleton set `{a}` is an element of the filter `pure a`. In other words, if we create a filter that consists only of the element `a`, then the set containing only `a` is indeed a member of this filter. This holds for any conceivable type and element of that type.
More concisely: For any type `α` and element `a` of type `α`, the singleton set `{a}` is contained in the filter `pure a`.
|
Mathlib.Order.Filter.Basic._auxLemma.177
theorem Mathlib.Order.Filter.Basic._auxLemma.177 :
∀ {α : Type u} {β : Type v} {f : Filter α} {m : α → β} {t : Set β}, (t ∈ Filter.map m f) = ({x | m x ∈ t} ∈ f) := by
sorry
This theorem in Lean 4 is asserting that for every type `α` and `β`, filter `f` on `α`, function `m` from `α` to `β`, and set `t` of type `β`, the set `t` is in the forward map of the filter `f` under the function `m` if and only if the set of all elements `x` in `α` such that `m(x)` belongs to `t` is in the filter `f`. In simpler terms, it states that `t` is in the image of filter `f` under `m` if and only if all pre-images of the elements of `t` under `m` are in `f`.
More concisely: For any type `α`, filter `f` on `α`, function `m` from `α` to `β`, and set `t` of type `β`, `t` is in the forward image of `f` under `m` if and only if the preimage of `t` under `m` is in `f`.
|
Filter.map_inf_le
theorem Filter.map_inf_le :
∀ {α : Type u} {β : Type v} {f g : Filter α} {m : α → β}, Filter.map m (f ⊓ g) ≤ Filter.map m f ⊓ Filter.map m g
This theorem states that for any types `α` and `β`, any two filters `f` and `g` on `α`, and any function `m` from `α` to `β`, the map of the infimum (greatest lower bound) of the two filters `f` and `g` under the function `m` is less than or equal to the infimum of the maps of filters `f` and `g` under the function `m`. In mathematical terms, this can be written as `m(f ⊓ g) ≤ m(f) ⊓ m(g)`.
More concisely: For any functions `m` from a type `α` to `β`, and filters `f` and `g` on `α`, the map of the infimum of `f` and `g` under `m` is less than or equal to the infimum of the maps of `f` and `g` under `m`, i.e., `m(f ⊓ g) ≤ m(f) ⊓ m(g)`.
|
Set.Nonempty.principal_neBot
theorem Set.Nonempty.principal_neBot : ∀ {α : Type u} {s : Set α}, s.Nonempty → (Filter.principal s).NeBot
The theorem `Set.Nonempty.principal_neBot` states that for any type `α` and any set `s` of that type, if `s` is nonempty, then the principal filter of `s` is not bottom. Here, a set is said to be nonempty if it contains at least one element, and a filter is not bottom if it's not the least element in the lattice of filters. In other words, the principal filter of a nonempty set always contains other filters.
More concisely: If a set is nonempty, then its principal filter is distinct from the bottom filter in the lattice of filters.
|
Filter.eventuallyEq_of_mem
theorem Filter.eventuallyEq_of_mem :
∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} {s : Set α}, s ∈ l → Set.EqOn f g s → l.EventuallyEq f g
This theorem states that for any two functions `f` and `g` of type `α → β`, if they are equal on a set `s` of type `α` and this set `s` is in a filter `l` of type `α`, then `f` and `g` are eventually equal with respect to the filter `l`. In mathematical terms, this means that for all elements in the filter `l`, the functions `f` and `g` will produce the same output. The "eventually equal" part (`=ᶠ[l]`) signifies that this equality holds for all elements in the filter `l` beyond a certain point.
More concisely: If functions `f` and `g` are equal on a set `s` that is in a filter `l`, then `f` and `g` are eventually equal with respect to the filter `l`, i.e., for all `x` in `l`, `f x = g x`.
|
Set.EqOn.eventuallyEq_of_mem
theorem Set.EqOn.eventuallyEq_of_mem :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {l : Filter α} {f g : α → β},
Set.EqOn f g s → s ∈ l → l.EventuallyEq f g
The theorem `Set.EqOn.eventuallyEq_of_mem` states that for any types `α` and `β`, any set `s` of type `α`, any filter `l` on `α`, and any two functions `f` and `g` from `α` to `β`, if `f` and `g` are equal on `s` and `s` is in the filter `l`, then `f` is eventually equal to `g` with respect to the filter `l`. In other words, at some point and thereafter in the sequence defined by the filter `l`, the values of `f` and `g` are the same for all elements in the set `s`.
More concisely: If `s` is a set in filter `l` over type `α`, and functions `f` and `g` from `α` to `β` agree on `s`, then there exists an index `n` such that for all `i ≥ n`, `f(s(i)) = g(s(i))`.
|
Filter.EventuallyEq.neg
theorem Filter.EventuallyEq.neg :
∀ {α : Type u} {β : Type v} [inst : Neg β] {f g : α → β} {l : Filter α},
l.EventuallyEq f g → l.EventuallyEq (fun x => -f x) fun x => -g x
This theorem states that for any types `α` and `β` and any instances of negation on `β`, given two functions `f` and `g` from `α` to `β` and a filter `l` on `α`, if `f` is eventually equal to `g` at filter `l`, then the function that maps each element of `α` to the negative of its image under `f` is eventually equal at filter `l` to the function that maps each element of `α` to the negative of its image under `g`. In other words, if `f` and `g` are nearly the same when observed through filter `l`, then the same applies to their negations.
More concisely: Given functions `f` and `g` from type `α` to negatable type `β`, and filter `l` on `α` such that `f` and `g` are eventual equal at `l`, their negations are also eventual equal at `l`.
|
Filter.mem_bot
theorem Filter.mem_bot : ∀ {α : Type u} {s : Set α}, s ∈ ⊥
This theorem states that for every type `α` and every set `s` of type `α`, `s` is an element of the smallest filter, denoted by `⊥`. In mathematical terms, this means that the smallest (or "bottom") filter contains every set from a given type.
More concisely: Every set belongs to the bottom filter.
|
Mathlib.Order.Filter.Basic._auxLemma.71
theorem Mathlib.Order.Filter.Basic._auxLemma.71 :
∀ {α : Type u} {p q : α → Prop} {f : Filter α},
(∀ᶠ (x : α) in f, p x ∧ q x) = ((∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in f, q x)
This theorem, `Mathlib.Order.Filter.Basic._auxLemma.71`, states that, for any type `α`, any propositions `p` and `q` about the elements of `α`, and any filter `f` on `α`, the event "for all `x` in the filter `f`, `p(x)` and `q(x)` holds" is equivalent to the conjunction of the two events "for all `x` in the filter `f`, `p(x)` holds" and "for all `x` in the filter `f`, `q(x)` holds". This shows that the proposition about the conjunction of two events in a filter can be split into two separate propositions about each event in the same filter.
More concisely: For any filter `f` on type `α`, proposition `p`, and proposition `q`, the statement "for all `x` in `f`, `p(x)` and `q(x)` hold" is equivalent to the conjunction of "for all `x` in `f`, `p(x)` holds" and "for all `x` in `f`, `q(x)` holds".
|
Filter.push_pull
theorem Filter.push_pull :
∀ {α : Type u} {β : Type v} (f : α → β) (F : Filter α) (G : Filter β),
Filter.map f (F ⊓ Filter.comap f G) = Filter.map f F ⊓ G
The theorem `Filter.push_pull` states that for all types `α` and `β`, for any function `f` from `α` to `β`, and for any filters `F` on `α` and `G` on `β`, the forward map of the intersection of `F` and the preimage filter of `f` under `G` is equal to the intersection of the forward map of `F` and `G`. In other words, this theorem expresses a distributive property of the filter map operation with respect to the intersection of filters, in the context of a function and its preimage.
More concisely: For any functions between types, the preimage filter of the function under the intersection of two filters is equal to the intersection of the function map and the filters.
|
Filter.tendsto_inf_right
theorem Filter.tendsto_inf_right :
∀ {α : Type u} {β : Type v} {f : α → β} {x₁ x₂ : Filter α} {y : Filter β},
Filter.Tendsto f x₂ y → Filter.Tendsto f (x₁ ⊓ x₂) y
The theorem `Filter.tendsto_inf_right` states that for any types `α` and `β`, a function `f` from `α` to `β`, and any filters `x₁`, `x₂` on `α` and a filter `y` on `β`, if `f` tends towards `y` as the input approaches `x₂`, then `f` also tends towards `y` as the input approaches the infimum (greatest lower bound) of filters `x₁` and `x₂`. This means that the limit of `f` at `x₂` is preserved even when considering the intersection of `x₁` and `x₂`.
More concisely: Given filters `x₁`, `x₂` on type `α` and a filter `y` on type `β`, if function `f` from `α` to `β` tends to `y` as inputs approach the infimum of `x₁` and `x₂`, then `f` tends to `y` as inputs approach the infimum of `{x₁, x₂}`.
|
Mathlib.Order.Filter.Basic._auxLemma.5
theorem Mathlib.Order.Filter.Basic._auxLemma.5 : ∀ {α : Type u} {f : Filter α}, (Set.univ ∈ f) = True
This theorem states that for any type `α` and any filter `f` on `α`, the universal set of `α` (i.e., the set containing all elements of `α`) is in the filter `f`. This is always true, regardless of the specific type or filter. In set-theoretic terms, this means that the filter `f` always includes the entire universe of discourse for the type `α`.
More concisely: For any type `α` and filter `f` on `α`, the universal set of `α` belongs to `f`.
|
Filter.iInf_neBot_of_directed'
theorem Filter.iInf_neBot_of_directed' :
∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} [inst : Nonempty ι],
Directed (fun x x_1 => x ≥ x_1) f → (∀ (i : ι), (f i).NeBot) → (iInf f).NeBot
This theorem states that given a directed family `f` of filters on type `α`, indexed by type `ι`, under the conditions where the index set `ι` is not empty and none of the filters in the family equals the bottom filter, it can be ensured that the indexed infimum of `f` will not equal the bottom filter. Here, a family of filters is considered directed if for any two filters in the family, there exists another filter in the family that is greater than or equal to both. The theorem also mentions an alternative version `iInf_neBot_of_directed` that assumes non-emptiness of `α` instead of `ι`.
More concisely: Given a non-empty directed family of filters `f` on a non-empty type `α`, none of which are the bottom filter, the indexed infimum of `f` is not the bottom filter.
|
Filter.seq_mem_seq
theorem Filter.seq_mem_seq :
∀ {α : Type u} {β : Type v} {f : Filter (α → β)} {g : Filter α} {s : Set (α → β)} {t : Set α},
s ∈ f → t ∈ g → s.seq t ∈ f.seq g
This theorem states that for all types `α` and `β`, given a filter `f` of functions from `α` to `β`, a filter `g` of `α`, a set `s` of functions from `α` to `β`, and a set `t` of `α`, if `s` is in `f` and `t` is in `g`, then the sequence operation on `s` and `t` is in the sequence operation on `f` and `g`. In simpler terms, if we have a set of functions and a set of inputs both contained in certain filters, then the set of outputs obtained by applying the functions to the inputs is also contained in a corresponding filter.
More concisely: If `f` is a filter of functions from `α` to `β`, `g` is a filter of `α`, `s ∈ f`, `t ∈ g`, and `s(x) = y` for all `x ∈ t`, then the set `{y | ∃x ∈ t, s(x) = y} ∈ sequence (f, g)`.
|
Mathlib.Order.Filter.Basic._auxLemma.90
theorem Mathlib.Order.Filter.Basic._auxLemma.90 :
∀ {α : Type u} {p : α → Prop} {f : Filter α}, (¬∃ᶠ (x : α) in f, p x) = ∀ᶠ (x : α) in f, ¬p x
This theorem states that for any type `α`, any property `p` of type `α`, and any filter `f` on `α`, the statement "there does not exist an `x` of type `α` in the filter `f` such that the property `p` holds for `x`" is equivalent to the statement "for all `x` of type `α` in the filter `f`, the property `p` does not hold for `x`". In other words, not having any element in a filter that satisfies a certain property is equivalent to all elements in that filter not satisfying the property.
More concisely: For any filter `f` on type `α` and property `p` of `α`, the filter `f` does not contain any element satisfying `p` if and only if no element in `f` satisfies `p`.
|
Filter.map_equiv_symm
theorem Filter.map_equiv_symm :
∀ {α : Type u} {β : Type v} (e : α ≃ β) (f : Filter β), Filter.map (⇑e.symm) f = Filter.comap (⇑e) f
The theorem `Filter.map_equiv_symm` states that for any types `α` and `β`, and for any equivalence `e : α ≃ β` and any filter `f` on `β`, the image of `f` under the inverse of `e` (obtained by applying the function `Filter.map` to the inverse of `e`) is the same as the preimage of `f` under `e` (obtained by applying the function `Filter.comap` to `e`). Essentially, this theorem is stating that mapping a filter through an inverse equivalence is the same as pulling back the filter through the original equivalence.
More concisely: For any equivalence `e : α ≃ β` and filter `f` on `β`, `Filter.map (inv e) f = Filter.comap e f`.
|
Filter.eventuallyLE_antisymm_iff
theorem Filter.eventuallyLE_antisymm_iff :
∀ {α : Type u} {β : Type v} [inst : PartialOrder β] {l : Filter α} {f g : α → β},
l.EventuallyEq f g ↔ l.EventuallyLE f g ∧ l.EventuallyLE g f
This theorem states that for any types `α` and `β`, and for any partial order on `β`, given a filter `l` on `α` and functions `f` and `g` from `α` to `β`, the functions `f` and `g` are eventually equal at filter `l` if and only if `f` is eventually less than or equal to `g` at filter `l` and `g` is eventually less than or equal to `f` at filter `l`. Here, "eventually" means that the condition holds except for possibly an initial segment of the sequence.
More concisely: For any types `α` and `β`, and for any partial order on `β`, two functions `f` and `g` from `α` to `β` are equal at a filter `l` if and only if one is less than or equal to the other at `l` and vice versa, up to an initial segment.
|
Filter.mem_pure
theorem Filter.mem_pure : ∀ {α : Type u} {a : α} {s : Set α}, s ∈ pure a ↔ a ∈ s
The theorem `Filter.mem_pure` states that for any type `α`, any element `a` of type `α`, and any set `s` of type `α`, the membership of `s` in the pure filter of `a` is equivalent to the membership of `a` in `s`. In other words, a set `s` is included in the pure filter of `a` if and only if `a` is an element of `s`. The pure filter of `a` is the collection of all sets that contain `a`.
More concisely: For any type α, element a of α, and set s of α, the set s is contained in the filter of a (i.e., the set of sets containing a) if and only if a is an element of s.
|
Filter.exists_mem_subset_iff
theorem Filter.exists_mem_subset_iff : ∀ {α : Type u} {f : Filter α} {s : Set α}, (∃ t ∈ f, t ⊆ s) ↔ s ∈ f
The theorem `Filter.exists_mem_subset_iff` states that for any type `α`, any filter `f` on `α`, and any set `s` of elements of type `α`, there exists a set `t` that is a member of the filter `f` and is a subset of `s` if and only if `s` is a member of the filter `f`. In other words, this theorem is describing a condition that a set `s` is in a filter `f` if and only if there's another set `t` in `f` that is contained within `s`.
More concisely: A set belongs to a filter if and only if there exists a subset of it that is in the filter.
|
Filter.union_mem_sup
theorem Filter.union_mem_sup : ∀ {α : Type u} {f g : Filter α} {s t : Set α}, s ∈ f → t ∈ g → s ∪ t ∈ f ⊔ g
The theorem `Filter.union_mem_sup` states that for any two filters `f` and `g` of a certain type `α`, and any two sets `s` and `t` of the same type, if set `s` is in filter `f` and set `t` is in filter `g`, then the union of sets `s` and `t` is in the supremum of filters `f` and `g`. In other words, this theorem asserts that the union of elements from two different filters resides within the filter formed by the supremum of these two filters.
More concisely: If filters `f` and `g` over set `α` have `s ∈ f` and `t ∈ g` for some sets `s` and `t` of type `α`, then `s ∪ t ∈ sup (f) ∧ g`.
|
Set.Finite.eventually_all
theorem Set.Finite.eventually_all :
∀ {α : Type u} {ι : Type u_2} {I : Set ι},
I.Finite →
∀ {l : Filter α} {p : ι → α → Prop}, (∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
The theorem `Set.Finite.eventually_all` is an alias for `Filter.eventually_all_finite`. It states that for any type `α` and any index type `ι`, given a finite set `I` of index type `ι`, for any filter `l` on `α` and any predicate `p` from `ι` to `α` to `Prop`, the property that for almost all `x` in `l`, the predicate `p i x` holds for all `i` in `I`, is equivalent to the property that for each `i` in `I`, for almost all `x` in `l`, the predicate `p i x` holds. In other words, switching the order of quantifiers over a finite index set and a filter doesn't change the truth value of the statement.
More concisely: For any filter on a type, a finite index set, and a predicate, the properties "for almost all elements in the filter, the predicate holds for all indices in a finite set" and "for each index in the finite set, for almost all elements in the filter, the predicate holds" are equivalent.
|
Filter.principal_empty
theorem Filter.principal_empty : ∀ {α : Type u}, Filter.principal ∅ = ⊥
This theorem states that for any type `α`, the principal filter of the empty set is equivalent to the bottom filter. In other words, the collection of all supersets of the empty set forms the most restrictive or trivial filter, often denoted by `⊥`, in the context of filters in set theory.
More concisely: The principal filter of the empty set is equal to the bottom filter for any type `α`.
|
Filter.eq_top_of_neBot
theorem Filter.eq_top_of_neBot : ∀ {α : Type u} [inst : Subsingleton α] (l : Filter α) [inst : l.NeBot], l = ⊤ := by
sorry
The theorem `Filter.eq_top_of_neBot` states that for any type `α` that is a `subsingleton` and any filter `l` on `α` which is not the bottom filter (`⊥`), `l` must equal the top filter (`⊤`). In simpler terms, this theorem states that there are only two possible filters on a subsingleton - the bottom filter and the top filter. If the type is empty, then these two filters are the same.
More concisely: For any subsingleton type `α` and non-bottom filter `l` on `α`, `l` equals the top filter `⊤`.
|
Filter.EventuallyEq.add
theorem Filter.EventuallyEq.add :
∀ {α : Type u} {β : Type v} [inst : Add β] {f f' g g' : α → β} {l : Filter α},
l.EventuallyEq f g → l.EventuallyEq f' g' → l.EventuallyEq (fun x => f x + f' x) fun x => g x + g' x
This theorem asserts that for any two pairs of functions `(f, g)` and `(f', g')` mapped from a type `α` to a type `β` that supports addition, if `f` is eventually equal to `g` and `f'` is eventually equal to `g'` under a certain filter `l`, then the function that maps `x` to `f(x) + f'(x)` is eventually equal to the function that maps `x` to `g(x) + g'(x)` under the same filter `l`. "Eventually equal" means that the functions are equal for all inputs from a certain point onward.
More concisely: If functions `f : α -> β` and `g : α -> β`, and functions `f' : α -> β` and `g' : α -> β` are eventually equal under filter `l`, then their sums `f + f' : α -> β` and `g + g' : α -> β` are eventually equal under the same filter `l`.
|
Filter.EventuallyEq.comp_tendsto
theorem Filter.EventuallyEq.comp_tendsto :
∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {γ : Type u_3} {f' : α → β},
l.EventuallyEq f f' → ∀ {g : γ → α} {lc : Filter γ}, Filter.Tendsto g lc l → lc.EventuallyEq (f ∘ g) (f' ∘ g)
The theorem `Filter.EventuallyEq.comp_tendsto` states that for any types `α`, `β`, and `γ`, any filter `l` on `α`, any functions `f` and `f'` from `α` to `β`, and any function `g` from `γ` to `α`, if `f` is eventually equal to `f'` at the filter `l`, then for any filter `lc` on `γ`, if `g` tends to `l` at `lc` (i.e., the limit of `g` as `lc` approaches `l` exists), then the composition of `f` and `g` is eventually equal to the composition of `f'` and `g` at the filter `lc`. In term of limit, if the function `g` converges to a limit `l` and at some point in the neighbourhood of this limit `f` is equal to `f'`, then the limit of the composition of `f` and `g` is the same as the limit of the composition of `f'` and `g`.
More concisely: If a function `f` is eventually equal to `f'` at a filter `l` on type `α`, and `g` tends to `l` at filter `lc` on type `γ`, then the composition `f ∘ g` is eventually equal to `f' ∘ g` at filter `lc`.
|
Filter.Eventually.frequently
theorem Filter.Eventually.frequently :
∀ {α : Type u} {f : Filter α} [inst : f.NeBot] {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, p x := by
sorry
This theorem states that for any type `α` and any filter `f` on `α`, provided that the filter `f` is not the bottom filter, if a property `p` holds "eventually" (meaning within a neighborhood of the filter) for elements `x` of type `α`, then there exists a neighborhood within the filter where the property `p` holds "frequently" (meaning on a dense subset).
More concisely: Given a type `α` and a non-bottom filter `f` on `α`, if property `p` holds "eventually" for `x` in `α` with respect to `f`, then there exists a dense subset `D` of `α` within `f` such that `p` holds for all elements in `D`.
|
Mathlib.Order.Filter.Basic._auxLemma.41
theorem Mathlib.Order.Filter.Basic._auxLemma.41 :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b = (a ⊓ b = ⊥)
This theorem states that for any type `α` that forms a semilattice with an infimum operation and has a smallest element, and for any two elements `a` and `b` of this type, `a` and `b` are disjoint (in the sense that any element `x` that is less than or equal to both `a` and `b` is also less than or equal to the smallest element of the type) if and only if the infimum of `a` and `b` is the smallest element of the type. The theorem therefore provides a characterization of disjointness in terms of the infimum operation and the smallest element of the type.
More concisely: For any semilattice with a smallest element `α`, elements `a` and `b` are disjoint if and only if their infimum is the smallest element of `α`.
|
Mathlib.Order.Filter.Basic._auxLemma.18
theorem Mathlib.Order.Filter.Basic._auxLemma.18 : ∀ {b a : Prop}, (∃ (_ : a), b) = (a ∧ b)
This theorem states that, for any two propositions 'a' and 'b', the existence of 'b' given 'a' is equivalent to the conjunction (logical "and") of 'a' and 'b'. In simple words, it means that 'b' exists if and only if both 'a' and 'b' are true.
More concisely: The theorem asserts that for all propositions 'a' and 'b', the existence of 'b' given 'a' is equivalent to 'a' and 'b' being true simultaneously.
|
Filter.neBot_of_le
theorem Filter.neBot_of_le : ∀ {α : Type u} {f g : Filter α} [hf : f.NeBot], f ≤ g → g.NeBot
This theorem states that for any type `α`, and for any two filters `f` and `g` on that type, if `f` is not the bottom filter (i.e., `f` is not the filter that includes all subsets of `α`), and if `f` is less than or equal to `g` (in the filter ordering), then `g` is also not the bottom filter. In other words, the theorem asserts that a filter which is greater than or equal to a non-bottom filter cannot be the bottom filter itself.
More concisely: If `α` is a type, `f` and `g` are filters on `α` with `f` non-bottom and `f ≤ g`, then `g` is also non-bottom.
|
Filter.Eventually.filter_mono
theorem Filter.Eventually.filter_mono :
∀ {α : Type u} {f₁ f₂ : Filter α}, f₁ ≤ f₂ → ∀ {p : α → Prop}, (∀ᶠ (x : α) in f₂, p x) → ∀ᶠ (x : α) in f₁, p x := by
sorry
This theorem states that for any type `α` and any two filters `f₁` and `f₂` on that type, if `f₁` is a subfilter of `f₂` (that is, `f₁` is less than or equal to `f₂`), then any property `p` that holds "eventually" (that is, outside of a finite set) in `f₂` also holds "eventually" in `f₁`. In other words, if a property is true in the larger filter `f₂`, it will also be true in the smaller filter `f₁`.
More concisely: If `f₁` is a subfilter of `f₂` on type `α`, then any property holding eventually in `f₂` also holds eventually in `f₁`.
|
Filter.mem_biInf_of_directed
theorem Filter.mem_biInf_of_directed :
∀ {α : Type u} {β : Type v} {f : β → Filter α} {s : Set β},
DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) s → s.Nonempty → ∀ {t : Set α}, t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i
The theorem `Filter.mem_biInf_of_directed` states that for all types `α` and `β`, for any function `f` mapping from `β` to a filter on `α`, and a set `s` of type `β`, if this set is directed with respect to the preimage under `f` of the relation "greater than or equal to", and the set `s` is not empty, then for any set `t` of type `α`, `t` belongs to the infimum filter over the set `s` with respect to `f` if and only if there exists an element `i` in `s` such that `t` belongs to the filter `f i`. In simpler terms, this theorem describes a condition under which a set is a member of an infimum filter generated by a directed, nonempty set of filters.
More concisely: For any type `α` and `β`, if `s` is a nonempty, directed set of filters on `α` with respect to the preimage under a function `f` from `β` to filters on `α`, then a set `t` belongs to the infimum filter of `s` with respect to `f` if and only if there exists an `i` in `s` such that `t` is in `f i`.
|
Filter.eventuallyEq_univ
theorem Filter.eventuallyEq_univ : ∀ {α : Type u} {s : Set α} {l : Filter α}, l.EventuallyEq s Set.univ ↔ s ∈ l := by
sorry
This theorem, `Filter.eventuallyEq_univ`, states that for any type `α`, any set `s` of type `α`, and any filter `l` on `α`, the set `s` is eventually equal to the universal set (i.e., `Set.univ`) under the filter `l` if and only if the set `s` belongs to the filter `l`. In other words, the set `s` contains all the elements that will eventually pass through the filter `l`.
More concisely: For any type `α`, set `s` of `α`, and filter `l` on `α`, `s` is equal to the universal set under filter `l` if and only if `s` belongs to `l`.
|
Mathlib.Order.Filter.Basic._auxLemma.94
theorem Mathlib.Order.Filter.Basic._auxLemma.94 :
∀ {α : Type u} {f : Filter α} [inst : f.NeBot] {p : Prop}, (∃ᶠ (x : α) in f, p) = p
This theorem states that for any type `α`, any filter `f` on `α` that is not bottom (i.e., does not contain all subsets of `α`), and any proposition `p`, the statement "There exists an element `x` in the filter `f` for which `p` holds" is equivalent to `p`. In other words, the property `p` holds eventually in the filter `f` if and only if `p` is true.
More concisely: For any filter `f` on a type `α` that is not bottom and any proposition `p` on `α`, the filter `f` contains an element `x` satisfying `p` if and only if `p` is true for all elements of `α`.
|
Mathlib.Order.Filter.Basic._auxLemma.153
theorem Mathlib.Order.Filter.Basic._auxLemma.153 :
∀ {ι : Type u_2} {α : ι → Type u_3} [inst : ∀ (j : ι), Nonempty (α j)] {i : ι} {f : Filter (α i)},
(Filter.comap (Function.eval i) f).NeBot = f.NeBot
This theorem states that for any index type `ι`, any function `α` from `ι` to some type, and any index `i` of type `ι`, given a filter `f` on the type `α i`, the filter obtained by precomposing `f` with the evaluation function at `i` is nontrivial if and only if `f` itself is nontrivial. Here, a nontrivial filter is one that does not collapse to contain only a single element. This theorem essentially says that the process of precomposing with the evaluation function preserves the nontriviality of a filter.
More concisely: For any index type `ι`, function `α : ι → Type`, index `i : ι`, and filter `f` on `α i`, the filter `f.map (eval i)` is nontrivial if and only if `f` is nontrivial.
|
Filter.mem_comap'
theorem Filter.mem_comap' :
∀ {α : Type u} {β : Type v} {f : α → β} {l : Filter β} {s : Set α},
s ∈ Filter.comap f l ↔ {y | ∀ ⦃x : α⦄, f x = y → x ∈ s} ∈ l
This theorem, `Filter.mem_comap'`, states that for every types `α` and `β`, every function `f` from `α` to `β`, every filter `l` of type `β`, and every set `s` of type `α`, the set `s` is in the co-domain of the function `f` with respect to the filter `l` if and only if the set of all `y` such that for each `x` in `α`, if `f(x)` equals `y` then `x` is in `s`, is in the filter `l`. Essentially, it's about the relationship between the filter and the set in the image and pre-image under a function `f`.
More concisely: For every function `f:` α -> β, filter `l` on β, and set `s` subset α, `s` is in the filter `l`'s image under `f` if and only if the set of all `y` in β such that the pre-image `{x in α | f(x) = y}` is a subset of `s`, is in `l`.
|
Filter.inf_principal
theorem Filter.inf_principal :
∀ {α : Type u} {s t : Set α}, Filter.principal s ⊓ Filter.principal t = Filter.principal (s ∩ t)
This theorem, named `Filter.inf_principal`, states that for any type `α` and any two sets `s` and `t` of type `α`, the intersection of the principal filters of `s` and `t` is equal to the principal filter of the intersection of `s` and `t`. In other words, the principal filter of the intersection of two sets is equivalent to the intersection of the principal filters of the individual sets.
More concisely: For any type `α` and sets `s` and `t` of type `α`, the principal filters of `s` and `t` have equal elements if and only if the intersection of `s` and `t` has the same principal filter.
|
Filter.ext
theorem Filter.ext : ∀ {α : Type u} {f g : Filter α}, (∀ (s : Set α), s ∈ f ↔ s ∈ g) → f = g
This theorem, known as `Filter.ext`, states that for any type `α` and any two filters `f` and `g` on `α`, if every set `s` of elements of type `α` is a member of the filter `f` if and only if `s` is a member of the filter `g`, then `f` and `g` are equal. In other words, two filters are considered equal if they contain the same sets.
More concisely: Two filters on a type `α` are equal if and only if they contain the same sets.
|
Filter.EventuallyLE.trans
theorem Filter.EventuallyLE.trans :
∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f g h : α → β},
l.EventuallyLE f g → l.EventuallyLE g h → l.EventuallyLE f h
This theorem, named `Filter.EventuallyLE.trans`, establishes the transitivity of the "eventually less than or equal to" (`≤ᶠ[l]`) relation over functions `f`, `g`, and `h` from a type `α` to a type `β`, given a preorder on `β` and a filter `l` on `α`. In simpler terms, it states that if `f` is eventually less than or equal to `g` under filter `l`, and `g` is eventually less than or equal to `h` under the same filter, then `f` is eventually less than or equal to `h` under filter `l`. This aligns with the concept of transitivity in mathematics.
More concisely: If `f ≤ᶠ[l] g` and `g ≤ᶠ[l] h` for functions `f, g, h : α → β` and filter `l` on `α`, then `f ≤ᶠ[l] h`.
|
Filter.comap_inf
theorem Filter.comap_inf :
∀ {α : Type u} {β : Type v} {g₁ g₂ : Filter β} {m : α → β},
Filter.comap m (g₁ ⊓ g₂) = Filter.comap m g₁ ⊓ Filter.comap m g₂
This theorem states that for all types `α` and `β`, given a function `m` from `α` to `β`, and two filters `g₁` and `g₂` on `β`, the comap of `m` on the infimum (i.e., the greatest lower bound) of `g₁` and `g₂` is equal to the infimum of the comap of `m` on `g₁` and `g₂`. In mathematical terms, this theorem is saying that the operation of taking the comap under a function distributes over the infimum operation on filters.
More concisely: For all types `α` and `β`, and functions `m` from `α` to `β`, the comap of `m` on the infimum of filters `g₁` and `g₂` on `β` equals the infimum of the comaps of `m` on `g₁` and `g₂`.
|
Filter.tendsto_pure
theorem Filter.tendsto_pure :
∀ {α : Type u} {β : Type v} {f : α → β} {a : Filter α} {b : β},
Filter.Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b
The theorem `Filter.tendsto_pure` states that for any given types `α` and `β`, a function `f` from `α` to `β`, a filter `a` on `α`, and a value `b` of type `β`, the function `f` tends towards `b` (in the sense of the `Filter.Tendsto` predicate) with respect to filter `a` if and only if it is eventually true in `a` that the function `f` applied to any element `x` of `α` equals `b`. In other words, for every element that eventually comes from `a`, the function `f` maps it to `b`.
More concisely: For any types `α` and `β`, a function `f:` `α` → `β`, a filter `a` on `α`, and a value `b` in `β`, `Filter.tendsto f a b` if and only if for every `x` in `α` that belongs to `a` infinitely often, `f x = b`.
|
Filter.mem_inf_of_right
theorem Filter.mem_inf_of_right : ∀ {α : Type u} {f g : Filter α} {s : Set α}, s ∈ g → s ∈ f ⊓ g
This theorem states that for any type `α`, and given two filters `f` and `g` on `α`, along with a set `s` of elements of type `α`, if the set `s` is a member of filter `g`, then `s` is also a member of the infimum (i.e., greatest lower bound) of filters `f` and `g`. In other words, if a set belongs to a filter, it will also belong to the infimum of that filter with any other filter.
More concisely: If filters `f` and `g` on type `α` have a common element set `s`, then `s` belongs to the infimum of `f` and `g`.
|
Mathlib.Order.Filter.Basic._auxLemma.20
theorem Mathlib.Order.Filter.Basic._auxLemma.20 : ∀ {α : Type u} {f : Filter α}, (¬f.NeBot) = (f = ⊥)
This theorem, `Mathlib.Order.Filter.Basic._auxLemma.20`, states that for any type `α` and any filter `f` on `α`, the negation of the statement "filter `f` is not the bottom element" is equivalent to saying "filter `f` is the bottom element". In other words, if `f` is not a non-empty filter (not NeBot), then `f` is the bottom filter, denoted by `⊥`. The bottom filter `⊥` is a special filter that contains all sets.
More concisely: The statement `Mathlib.Order.Filter.Basic._auxLemma.20` in Lean 4 asserts that for any filter `f` on type `α`, `~(f ≠ ⊥)` is equivalent to `f = ⊥`.
|
Filter.Eventually.set_eq
theorem Filter.Eventually.set_eq :
∀ {α : Type u} {s t : Set α} {l : Filter α}, (∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t) → l.EventuallyEq s t
This theorem, named `Filter.Eventually.set_eq`, expresses that for any set `s` and `t` of a certain type `α`, and a filter `l` on that type, if it is always the case that an element `x` of `α` is in `s` if and only if `x` is in `t` (under the filter `l`), then the sets `s` and `t` are eventually equal under that filter. In other words, it states that two sets are considered equal under a filter if all elements from the filter satisfy the condition of being in one set if and only if they are in the other.
More concisely: If for all `x` in the filter `l` on type `α`, `x` is in set `s` if and only if `x` is in set `t`, then sets `s` and `t` are eventually equal under filter `l`.
|
Function.Semiconj.filter_map
theorem Function.Semiconj.filter_map :
∀ {α : Type u} {β : Type v} {f : α → β} {ga : α → α} {gb : β → β},
Function.Semiconj f ga gb → Function.Semiconj (Filter.map f) (Filter.map ga) (Filter.map gb)
The theorem `Function.Semiconj.filter_map` states that for any types `α` and `β`, and for any functions `f : α → β`, `ga : α → α`, and `gb : β → β`, if `f` semiconjugates `ga` to `gb` (meaning that applying `f` after `ga` is the same as applying `gb` after `f`), then the function that maps a filter through `f` also semiconjugates the function that maps a filter through `ga` to the function that maps a filter through `gb`. In other words, the property of semiconjugation is preserved when we move from the world of functions to the world of filter transformations.
More concisely: If functions `f : α → β`, `ga : α → α`, and `gb : β → β` satisfy `ga ∘ f = f ∘ gb`, then `(filter.map f) (filter.map ga) = filter.map (gb ∘ f)`.
|
Finset.eventually_all
theorem Finset.eventually_all :
∀ {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ι → α → Prop},
(∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
This theorem, named `Finset.eventually_all`, is an alias of `Filter.eventually_all_finset`. It states that for all finite sets `I` of type `ι`, a filter `l` on a type `α`, and a property `p` that takes an element of `ι` and `α`, the property `p` holds eventually for all `x` in the filter `l` and all `i` in the set `I` if and only if for all `i` in the set `I`, the property `p` holds eventually for all `x` in the filter `l`. In other words, it's asserting the equivalence of "eventually for all" and "for all, eventually" in this context.
More concisely: For a finite set I, filter l on α, and property p, p eventually holds for all x in l and i in I if and only if for all i in I, p eventually holds for all x in l.
|
Mathlib.Order.Filter.Basic._auxLemma.36
theorem Mathlib.Order.Filter.Basic._auxLemma.36 :
∀ {α : Type u} {s : Set α} {f : Filter α}, (f ≤ Filter.principal s) = (s ∈ f)
The theorem `Mathlib.Order.Filter.Basic._auxLemma.36` states that for any type `α`, any set `s` of type `α`, and any filter `f` of type `α`, the filter `f` is less than or equal to the principal filter of `s` if and only if `s` is a member of the filter `f`. In other words, the filter `f` contains all supersets of `s` if and only if `s` is one of the sets in the filter `f`. This provides a condition for a filter to be a superset of another filter in terms of element membership.
More concisely: A filter `f` of a type `α` contains a set `s` if and only if `s` is a subset of the principal filter of `s` and `s` is an element of `f`.
|
Filter.map_swap4_eq_comap
theorem Filter.map_swap4_eq_comap :
∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {f : Filter ((α × β) × γ × δ)},
Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) f =
Filter.comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) f
This theorem, `Filter.map_swap4_eq_comap`, states that for every filter `f` over a type of four-tuple `((α × β) × γ × δ)`, the filter obtained by mapping `f` via the function that swaps and re-pairs the elements of the four-tuple — that is, a function that takes an input four-tuple `((a, b), c, d)` and returns `((a, c), b, d)` — is equivalent to the filter obtained by co-mapping `f` with the same function. This theorem is particularly helpful when working with uniformities in mathematics.
More concisely: For any filter `f` over the type `((α × β) × γ × δ)`, the filters obtained by applying `map` and `comap` with the function swapping and re-pairing the elements are equal.
|
Filter.tendsto_def
theorem Filter.tendsto_def :
∀ {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
Filter.Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f ⁻¹' s ∈ l₁
The theorem `Filter.tendsto_def` states that for any two types `α` and `β`, and any function `f` from `α` to `β`, and any filters `l₁` on `α` and `l₂` on `β`, the function `f` tends to filter `l₂` along filter `l₁` if and only if for every set `s` in the filter `l₂`, the preimage of `s` under `f` is in the filter `l₁`. In other words, the theorem provides a characterization of the concept of limit of a function in terms of preimages of sets.
More concisely: A function between two types tends to a filter if and only if the preimage of every set in the filter is in the filter through the domain.
|
Filter.mem_inf_of_left
theorem Filter.mem_inf_of_left : ∀ {α : Type u} {f g : Filter α} {s : Set α}, s ∈ f → s ∈ f ⊓ g
The theorem `Filter.mem_inf_of_left` states that for any type `α`, any filters `f` and `g` of type `α`, and any set `s` of type `α`, if `s` is in `f`, then `s` is in the infimum (intersection) of `f` and `g`. This expresses the intuitive idea that if a set is contained in a filter, then it is also contained in the intersection of that filter with any other filter.
More concisely: If `s` is in filter `f` and `g` is another filter on type `α`, then `s` is in the intersection `f ∩ g`.
|
Filter.NeBot.ne
theorem Filter.NeBot.ne : ∀ {α : Type u} {f : Filter α}, f.NeBot → f ≠ ⊥
This theorem states that for any type `α` and any filter `f` of type `α`, if `f` is not a "bottom" filter (as denoted by `Filter.NeBot f`), then `f` is not equal to `⊥`. In other words, if `f` is not a trivial (or empty) filter, then `f` is not the least element in the order of filters, which is represented by `⊥` in Lean.
More concisely: If `f` is a non-bottom filter on type `α`, then `f ≠ ⊥`.
|
Filter.principal_singleton
theorem Filter.principal_singleton : ∀ {α : Type u} (a : α), Filter.principal {a} = pure a
The theorem `Filter.principal_singleton` states that for any type `α` and any element `a` of type `α`, the principal filter of the singleton set containing `a` is equal to the pure function applied to `a`. In other words, the collection of all supersets of a singleton set `{a}` is equivalent to creating a function that always returns `a`.
More concisely: For any type α and element a of α, the principal filter of the singleton set {a} equals the constant function mapping to a.
|
Filter.disjoint_iff
theorem Filter.disjoint_iff : ∀ {α : Type u} {f g : Filter α}, Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t
The theorem `Filter.disjoint_iff` states that for any type `α` and any two filters `f` and `g` on that type, `f` and `g` are disjoint if and only if there exist sets `s` and `t` such that `s` is in `f`, `t` is in `g`, and `s` and `t` are disjoint. Here, 'disjoint' in the context of two elements of a lattice means that their infimum (or greatest lower bound) is the bottom element of the lattice. This is a generalization of the notion of disjoint sets.
More concisely: Two filters `f` and `g` on a type `α` are disjoint if and only if there exist sets `s` in `f` and `t` in `g` such that `s ∩ t = ⊥`, where `⊥` denotes the bottom element of the lattice.
|
Filter.mem_comap
theorem Filter.mem_comap :
∀ {α : Type u} {β : Type v} {g : Filter β} {m : α → β} {s : Set α}, s ∈ Filter.comap m g ↔ ∃ t ∈ g, m ⁻¹' t ⊆ s
This theorem states that for any types `α` and `β`, any filter `g` of type `β`, any function `m` from `α` to `β`, and any set `s` of `α`, the set `s` belongs to the filter generated by the preimage of `g` under `m`, if and only if there exists a set `t` in `g` such that the preimage of `t` under `m` is a subset of `s`. Here, `m ⁻¹' t` denotes the preimage of `t` under `m`, which is the set of all elements in `α` that `m` sends to elements in `t`.
More concisely: For any types `α` and `β`, filter `g` of `β`, function `m` from `α` to `β`, and set `s` of `α`, `s` belongs to the filter generated by `m⁻¹' g` if and only if there exists `t` in `g` such that `m⁻¹' t` is a subset of `s`.
|
Mathlib.Order.Filter.Basic._auxLemma.17
theorem Mathlib.Order.Filter.Basic._auxLemma.17 : ∀ {α : Sort u_1} {p : α → Prop}, (¬∀ (x : α), p x) = ∃ x, ¬p x := by
sorry
This theorem states that, for any type `α` and any predicate `p` on `α`, the assertion that it is not the case that `p` holds for all `x` of type `α` is equivalent to there existing an `x` of type `α` for which `p` does not hold. In other words, if there exists a member of type `α` that does not satisfy the predicate `p`, then it is not true that `p` is satisfied by all members of `α`, and conversely, if it is not true that `p` is satisfied by all members of `α`, then there exists a member of `α` that does not satisfy `p`.
More concisely: For any type `α` and predicate `p` on `α`, the negation of "∀x ∈ α, p(x)" is equivalent to the existence of an `x ∈ α` such that not `p(x)`.
|
Filter.tendsto_congr
theorem Filter.tendsto_congr :
∀ {α : Type u} {β : Type v} {f₁ f₂ : α → β} {l₁ : Filter α} {l₂ : Filter β},
(∀ (x : α), f₁ x = f₂ x) → (Filter.Tendsto f₁ l₁ l₂ ↔ Filter.Tendsto f₂ l₁ l₂)
The theorem `Filter.tendsto_congr` states that for any two functions `f₁` and `f₂` from a type `α` to type `β`, and given filters `l₁` on `α` and `l₂` on `β`, if every element of `α` is mapped to the same value by both `f₁` and `f₂`, then `f₁` tends towards `l₂` along `l₁` if and only if `f₂` also tends towards `l₂` along `l₁`. In other words, if two functions are equal at each input, their corresponding limits with respect to the same input and output filters are also equivalent.
More concisely: If two functions map the same element to the same value for all elements in filters `l₁` on `α` and `l₂` on `β`, then `f₁` tends towards `l₂` along `l₁` if and only if `f₂` also tends towards `l₂` along `l₁`.
|
Filter.Eventually.congr
theorem Filter.Eventually.congr :
∀ {α : Type u} {f : Filter α} {p q : α → Prop},
(∀ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, p x ↔ q x) → ∀ᶠ (x : α) in f, q x
This theorem, `Filter.Eventually.congr`, states that for any type `α`, any filter `f` of `α`, and any propositions `p` and `q` that depend on `α`, if `p` holds for all elements of `f` eventually (`∀ᶠ (x : α) in f, p x`) and if it is also true that `p` eventually holds for all elements of `f` if and only if `q` does (`∀ᶠ (x : α) in f, p x ↔ q x`), then `q` also holds for all elements of `f` eventually (`∀ᶠ (x : α) in f, q x`). Basically, this theorem talks about the congruence of two propositions in the context of eventually in a filter.
More concisely: If a filter `f` of type `α` satisfies `∀ᶠ (x : α) in f, p x` and `p x ↔ q x` for all `x : α`, then `∀ᶠ (x : α) in f, q x`.
|
Filter.Eventually.exists_mem
theorem Filter.Eventually.exists_mem :
∀ {α : Type u} {p : α → Prop} {f : Filter α}, (∀ᶠ (x : α) in f, p x) → ∃ v ∈ f, ∀ y ∈ v, p y
This theorem states that for any type `α`, any property `p` on elements of `α`, and any filter `f` on `α`, if it's eventually the case in filter `f` that property `p` holds for `α`, then there exists a subset `v` in filter `f` such that property `p` holds for all elements in `v`. In other words, if a property is eventually true in a filter, you can find a set within that filter where the property is always true.
More concisely: If `p` is a property of type `α`, and `f` is a filter on `α` such that for all `x ∈ α`, there exists a finite sequence `(x₁, ..., xₖ)` in `f` with `xₖ ∈ f` and `p(xₖ)` holds, then there exists a subset `v ∈ f` such that for all `x ∈ v`, `p(x)` holds.
|
Mathlib.Order.Filter.Basic._auxLemma.92
theorem Mathlib.Order.Filter.Basic._auxLemma.92 : ∀ {α : Type u} (f : Filter α), (∃ᶠ (x : α) in f, True) = f.NeBot := by
sorry
This theorem, named `Mathlib.Order.Filter.Basic._auxLemma.92`, states that for every type `α` and a filter `f` on `α`, the proposition "there exists some `x` in `f` for which `True` holds" is equivalent to the filter `f` being not bottom (i.e., not the smallest filter or not empty). This essentially shows a condition under which a filter is considered non-empty.
More concisely: For every type `α` and filter `f` on `α`, the proposition "there exists an element in `f`" is equivalent to `f` not being the bottom filter.
|
Filter.tendsto_iInf
theorem Filter.tendsto_iInf :
∀ {α : Type u} {β : Type v} {ι : Sort x} {f : α → β} {x : Filter α} {y : ι → Filter β},
Filter.Tendsto f x (⨅ i, y i) ↔ ∀ (i : ι), Filter.Tendsto f x (y i)
The theorem `Filter.tendsto_iInf` states that for any types `α` and `β`, index type `ι`, function `f` from `α` to `β`, a filter `x` on `α`, and a indexed collection of filters `y` on `β`, the function `f` has the property of tending towards the infimum of the filters `y` (denoted by `(⨅ i, y i)`) if and only if it tends towards each individual filter in the collection `y`. In other words, the function `f` has the limit at each filter of the collection `y` if it has the limit at the infimum of these filters.
More concisely: For any types `α` and `β`, index type `ι`, function `f` from `α` to `β`, filter `x` on `α`, and indexed collection of filters `y` on `β`, `f` tends towards the infimum of `y` if and only if it tends towards each `y_i`.
|
Filter.eq_or_neBot
theorem Filter.eq_or_neBot : ∀ {α : Type u} (f : Filter α), f = ⊥ ∨ f.NeBot
This theorem states that for any filter `f` of an arbitrary type `α`, either `f` is equal to the bottom filter (denoted as `⊥`), or `f` is not the bottom filter (`Filter.NeBot f`). This is a version of the equality or inequality law (`eq_or_ne`) which uses `Filter.NeBot` as the second alternative option, and it is intended to be used as an instance.
More concisely: For any filter `f` on type `α`, either `f = ⊥` or `f ≠ ⊥`.
|
Filter.comap_iSup
theorem Filter.comap_iSup :
∀ {α : Type u} {β : Type v} {ι : Sort u_2} {f : ι → Filter β} {m : α → β},
Filter.comap m (iSup f) = ⨆ i, Filter.comap m (f i)
This theorem states that for any types `α`, `β`, and an indexed set `ι`, given a function `f` from `ι` to the set of filters on `β` and a function `m` from `α` to `β`, the filter obtained by applying the function `m` to the indexed supremum of the filter function `f` (`Filter.comap m (iSup f)`) is equal to the supremum of the filters obtained by applying the function `m` to each filter in the range of `f` (`⨆ i, Filter.comap m (f i)`). This is essentially distributing the comap operation over the supremum of filters.
More concisely: For any types `α`, `β`, indexed set `ι`, function `f` from `ι` to filters on `β`, and function `m` from `α` to `β`, `Filter.comap m (iSup f)` is equal to `⨆ i, Filter.comap m (f i)`.
|
Filter.eventually_of_mem
theorem Filter.eventually_of_mem :
∀ {α : Type u} {f : Filter α} {P : α → Prop} {U : Set α}, U ∈ f → (∀ x ∈ U, P x) → ∀ᶠ (x : α) in f, P x
This theorem, `Filter.eventually_of_mem`, states that for any type `α`, any filter `f` on `α`, any proposition `P` depending on an element of `α`, and any set `U` of elements of `α`: if `U` belongs to the filter `f` and the proposition `P` holds for all elements `x` in `U`, then `P` will eventually hold for all elements `x` in the filter `f`. This concept of "eventually" comes from the idea of filters which is a mathematical construction used in analysis and topology to generalize notions of limit and neighborhood.
More concisely: If a set belongs to a filter and its elements satisfy a proposition, then every element in the filter eventually satisfies the proposition.
|
Mathlib.Order.Filter.Basic._auxLemma.157
theorem Mathlib.Order.Filter.Basic._auxLemma.157 : ∀ {p : Prop} {q : p → Prop} (h : p), (∀ (h' : p), q h') = q h := by
sorry
This theorem states that for any proposition `p` and a function `q` dependent on `p`, given that `p` holds true (represented by `h : p`), the proposition that `q` holds true for all possible values of `p` (`∀ (h' : p), q h'`) is equivalent to `q` holding true for the specific instance of `p` being true (`q h`).
More concisely: For any proposition `p` and dependent function `q`, `∀ (h : p) , q h ↔ q (h : p)` holds. (This statement asserts the equivalence of the dependent function `q` being true for all instances of `p` and the specific instance where `p` holds.)
|
Filter.map_id
theorem Filter.map_id : ∀ {α : Type u} {f : Filter α}, Filter.map id f = f
This theorem, `Filter.map_id`, states that for any type `α` and any filter `f` of type `α`, the map of `f` with the identity function (`id`) is equal to `f` itself. In other words, applying the identity function to each element of the filter does not change the filter. This reflects the mathematical concept that mapping a set or collection through the identity function always results in the same set or collection.
More concisely: For any filter `f` on type `α`, `map f id = f`.
|
Filter.NeBot.comap_of_range_mem
theorem Filter.NeBot.comap_of_range_mem :
∀ {α : Type u} {β : Type v} {f : Filter β} {m : α → β}, f.NeBot → Set.range m ∈ f → (Filter.comap m f).NeBot := by
sorry
This theorem states that for any two types `α` and `β`, any filter `f` on `β`, and any function `m` from `α` to `β`, if the filter `f` is not the bottom filter and the range of function `m` is in the filter `f`, then the preimage filter (the filter obtained by applying the function `m` backwards to `f`) is also not the bottom filter. In other words, under these conditions, applying a function backwards to a filter does not result in the trivial (or bottom) filter.
More concisely: If `f` is a non-bottom filter on type `β`, and the range of function `m` from type `α` to `β` is included in `f`, then the preimage filter of `f` under `m` is also a non-bottom filter.
|
Filter.EventuallyEq.filter_mono
theorem Filter.EventuallyEq.filter_mono :
∀ {α : Type u} {β : Type v} {l l' : Filter α} {f g : α → β}, l.EventuallyEq f g → l' ≤ l → l'.EventuallyEq f g := by
sorry
This theorem states that for any two types `α` and `β`, any two filters `l` and `l'` on `α`, and any two functions `f` and `g` from `α` to `β`, if `f` is eventually equal to `g` at filter `l` and filter `l'` is a subfilter of `l`, then `f` is also eventually equal to `g` at filter `l'`. In other words, if two functions are eventually equal under a certain filter, they remain eventually equal when we move to a finer (sub)filter.
More concisely: If `l` is a filter on type `α`, `l'` is a subfilter of `l`, functions `f` and `g` from `α` to type `β`, and `f` is eventually equal to `g` at filter `l`, then `f` is eventually equal to `g` at filter `l'`.
|
Filter.sInter_mem
theorem Filter.sInter_mem :
∀ {α : Type u} {f : Filter α} {s : Set (Set α)}, s.Finite → (s.sInter ∈ f ↔ ∀ U ∈ s, U ∈ f)
The theorem, `Filter.sInter_mem`, states that for any type `α`, any filter `f` on `α`, and any finite set `s` of subsets of `α`, the intersection of all elements in the set `s` belongs to the filter `f` if and only if all elements (subsets `U`) in the set `s` belong to the filter `f`. This theorem essentially captures the principle that a filter contains the intersection of any finite collection of its elements.
More concisely: A filter `f` on a type `α` contains the intersection of any finite number of its elements if and only if each element in the finite set of subsets belongs to the filter. In Lean 4, this is expressed as the theorem `Filter.sInter_mem`.
|
Filter.map_comm
theorem Filter.map_comm :
∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ},
ψ ∘ φ = ρ ∘ θ → ∀ (F : Filter α), Filter.map ψ (Filter.map φ F) = Filter.map ρ (Filter.map θ F)
This theorem states that for any types `α`, `β`, `γ`, and `δ`, and any functions `φ` from `α` to `β`, `θ` from `α` to `γ`, `ψ` from `β` to `δ`, and `ρ` from `γ` to `δ`, if the composition of `ψ` and `φ` is equal to the composition of `ρ` and `θ`, then for any filter `F` on `α`, the result of mapping `F` through `φ` and then `ψ` is the same as the result of mapping `F` through `θ` and then `ρ`. In other words, if two pairs of functions are equivalent when composed, they induce the same transformation on filters.
More concisely: If for functions `φ: α → β`, `θ: α → γ`, `ψ: β → δ`, and `ρ: γ → δ` hold that `ψ ∘ φ = ρ ∘ θ`, then for any filter `F` on `α`, `map (φ ∘ ψ) F = map (θ ∘ ρ) F`.
|
Filter.frequently_iff_neBot
theorem Filter.frequently_iff_neBot :
∀ {α : Type u} {l : Filter α} {p : α → Prop}, (∃ᶠ (x : α) in l, p x) ↔ (l ⊓ Filter.principal {x | p x}).NeBot := by
sorry
This theorem states that for any type `α`, any filter `l` on `α`, and any property `p` of elements of `α`, the statement "there exist frequently (in the sense of the filter `l`) elements `x` of `α` such that `p(x)` holds" is equivalent to the statement "the infimum (or intersection) of the filter `l` and the principal filter of the set of elements `x` for which `p(x)` holds is not the bottom filter". The principal filter of a set `s` is defined as the collection of all supersets of `s`, and the bottom (or trivial) filter is the filter that contains all subsets of the set.
More concisely: For any type `α`, filter `l` on `α`, and property `p` of elements of `α`, the filter `l` intersects the principal filter of elements `x` with `p(x)` holding is non-empty if and only if the infimum of `l` is not the bottom filter.
|
Filter.eventually_inf_principal
theorem Filter.eventually_inf_principal :
∀ {α : Type u} {f : Filter α} {p : α → Prop} {s : Set α},
(∀ᶠ (x : α) in f ⊓ Filter.principal s, p x) ↔ ∀ᶠ (x : α) in f, x ∈ s → p x
The theorem `Filter.eventually_inf_principal` expresses a property about events in filters of a certain set in type `α`. It states that for any type `α`, any filter `f` of type `α`, any property `p` that elements of type `α` may satisfy, and any set `s` of elements of type `α`, the property `p` holds eventually (at all but finitely many elements) for the elements of the intersection of filter `f` and the principal filter of set `s` if and only if the property `p` holds eventually in filter `f` for those elements that belong to set `s`. Here, the principal filter of a set is defined as the collection of all supersets of the set.
More concisely: For any filter `f` on type `α`, set `s`, and property `p`, if `p` holds eventually in `f` for all elements of `s`, then `p` holds eventually in the intersection of `f` and the principal filter of `s`. Conversely, if `p` holds eventually in `f` for all elements of `s`, then it holds eventually in the intersection of `f` and the principal filter of `s`.
|
Mathlib.Order.Filter.Basic._auxLemma.37
theorem Mathlib.Order.Filter.Basic._auxLemma.37 :
∀ {α : Type u} [inst : PartialOrder α] {a b : α}, (a = b) = (a ≤ b ∧ b ≤ a)
This theorem from the Mathlib library titled "Order.Filter.Basic._auxLemma.37" states that for any type `α`, which has a partial ordering, and for any two elements 'a' and 'b' of type `α`, 'a' is equal to 'b' if and only if 'a' is less than or equal to 'b' and 'b' is less than or equal to 'a'. In other words, in a partial order, two elements are equal if, and only if, they are each less than or equal to the other.
More concisely: In a partial ordering, two elements are equivalent if and only if they mutually satisfy the relation of being less than or equal to each other.
|
Filter.Tendsto.le_comap
theorem Filter.Tendsto.le_comap :
∀ {α : Type u} {β : Type v} {f : α → β} {l₁ : Filter α} {l₂ : Filter β},
Filter.Tendsto f l₁ l₂ → l₁ ≤ Filter.comap f l₂
The theorem `Filter.Tendsto.le_comap` is an alias for the forward direction of `Filter.tendsto_iff_comap`. This theorem states that for every type `α` and `β`, given a function `f` from `α` to `β`, and given two filters `l₁` over `α` and `l₂` over `β`, if `f` tends towards `l₂` as `l₁` approaches (as stated by `Filter.Tendsto f l₁ l₂`), then `l₁` is less than or equal to the filter `l₂` pre-composed with `f` (as stated by `l₁ ≤ Filter.comap f l₂`). Essentially, this means that any neighborhood in `l₁` is mapped into a neighborhood in `l₂` under the function `f`.
More concisely: If a function `f` tends towards a filter `l₂` as a filter `l₁` approaches, then `l₁` is contained in the filter obtained by pre-composing `l₂` with `f`.
|
Filter.inter_mem_iff
theorem Filter.inter_mem_iff : ∀ {α : Type u} {f : Filter α} {s t : Set α}, s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f
This theorem, named `Filter.inter_mem_iff`, states that for any type `α`, any filter `f` on `α`, and any two sets `s` and `t` of `α`, the intersection of `s` and `t` belongs to the filter `f` if and only if both `s` and `t` belong to the filter `f`. In other words, the intersection of two sets is a member of a given filter iff each of the sets is a member of the filter.
More concisely: For any filter `f` on a type `α`, and sets `s` and `t` in `α`, `s ∩ t ∈ f` if and only if `s, t ∈ f`.
|
Filter.map_bot
theorem Filter.map_bot : ∀ {α : Type u} {β : Type v} {m : α → β}, Filter.map m ⊥ = ⊥
The theorem `Filter.map_bot` states that for any types `α` and `β`, and any function `m` from `α` to `β`, the result of applying the forward map of a filter on the function `m` and the bottom filter (represented as `⊥`) is the bottom filter itself. In other words, the forward map of the bottom filter under any function is the bottom filter.
More concisely: For any function `m` from type `α` to type `β`, the forward map of the bottom filter on `α` is the bottom filter on `β`.
|