Filter.Tendsto.of_smallSets
theorem Filter.Tendsto.of_smallSets :
∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {s : α → Set β} {f : α → β},
Filter.Tendsto s la lb.smallSets → (∀ᶠ (x : α) in la, f x ∈ s x) → Filter.Tendsto f la lb
This Lean 4 theorem, `Filter.Tendsto.of_smallSets`, represents a generalized version of the Squeeze Theorem, also known as the Sandwich Theorem. The theorem states that if `s` is a family of sets indexed by type `α` that maps to a set of type `β`, and this family of sets tends to the filter of small sets of `lb` along the filter `la`, and if there exists a function `f` that maps from `α` to `β` such that the value `f x` is in the set `s x` for all `x` in `α` eventually along `la`, then the function `f` tends to the filter `lb` along `la`. In simpler terms, if `f(x)` is always within the set `s(x)` and `s(x)` is closing in on a limit, then `f(x)` will also close in on that same limit.
In the special case where `s x` is the closed interval `[g x, h x]` for some functions `g` and `h` that converge to the same limit point `y`, we retrieve the classic Squeeze Theorem: if a function `f(x)` is always bounded by two other functions `g(x)` and `h(x)` which converge to the same limit at a certain point, then `f(x)` must also converge to that limit at that point.
More concisely: If a family of sets `s x` that tend to the filter of small sets along filter `la`, and for all `x`, `f x` is in `s x` eventually along `la`, then `f` tends to the filter `lb` along `la`.
|
Filter.Tendsto.image_smallSets
theorem Filter.Tendsto.image_smallSets :
∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {f : α → β},
Filter.Tendsto f la lb → Filter.Tendsto (fun x => f '' x) la.smallSets lb.smallSets
This theorem, named as "Filter.Tendsto.image_smallSets", states that for any type `α` and `β`, any two filters `la` and `lb`, and any function `f` from `α` to `β`, if `f` tends to map elements from filter `la` to filter `lb` (i.e., `Filter.Tendsto f la lb`), then the function that maps elements `x` to the image of `x` under `f` (`fun x => f '' x`) also tends to map elements from the small sets of `la` to the small sets of `lb` (i.e., `Filter.Tendsto (fun x => f '' x) la.smallSets lb.smallSets`). In other words, if `f` preserves the limit behavior from `la` to `lb`, then it also preserves the limit behavior from the small sets of `la` to the small sets of `lb`.
More concisely: If a function `f` tends to map elements from filter `la` to filter `lb` in type `β`, then the function mapping each element `x` in `α` to its image `f '' x` tends to map small sets of `la` to small sets of `lb`.
|
Filter.HasBasis.smallSets
theorem Filter.HasBasis.smallSets :
∀ {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → l.smallSets.HasBasis p fun i => (s i).powerset
This theorem states that for any type `α`, for any filter `l` on α, and any function `p` from a certain sort `ι` to propositions and another function `s` from the same sort `ι` to sets of α, if the filter `l` has a basis defined by `p` and `s` then the filter of all small sets of `l` (i.e., `Filter.smallSets l` which is defined as the largest filter containing all powersets of members of `l`), also has a basis defined by `p` and the function that maps `i` in `ι` to the powerset of `s i`. Here, `𝒫 s i` denotes the powerset of the set `s i`.
In simpler terms, the theorem says that if you can describe a filter `l` using some property and a set of basis, then you can also describe the filter of all small sets or subcollections of `l` using the same property and the powersets of the same set of basis.
More concisely: Given a filter `l` on type `α` with basis `(p : ι → Prop)` and `(s : ι → Set α)`, the filter of small sets `Filter.smallSets l` has basis `(p : ι → Prop)` and the function mapping `i` to the powerset `𝒫 (s i)`.
|
Mathlib.Order.Filter.SmallSets._auxLemma.11
theorem Mathlib.Order.Filter.SmallSets._auxLemma.11 :
∀ {α : Type u} {p : α → Prop}, (∀ᶠ (x : α) in ⊤, p x) = ∀ (x : α), p x
This theorem states that for any type `α` and any property `p` that elements of `α` can have, the proposition that "almost every element `x` of type `α` satisfies `p`" is equivalent to the proposition that "every element `x` of type `α` satisfies `p`". In more traditional mathematical terms, if `p` is a predicate over a set `α`, then the statement "for almost every `x` in `α`, `p(x)` holds" is equivalent to "for all `x` in `α`, `p(x)` holds". Here, the 'almost-every' stipulation is defined with respect to the trivial filter `⊤`, which in this context simply means "all of `α`".
More concisely: For any type `α` and property `p` over `α`, the statement "for almost all `x` in `α`, `p(x)` holds" is equivalent to "for all `x` in `α`, `p(x)` holds".
|
Filter.tendsto_smallSets_iff
theorem Filter.tendsto_smallSets_iff :
∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {f : α → Set β},
Filter.Tendsto f la lb.smallSets ↔ ∀ t ∈ lb, ∀ᶠ (x : α) in la, f x ⊆ t
This theorem states that a function `g` (denoted as `f` in the theorem) from a type `α` to a set of type `β` converges to the 'small sets' of a filter `lb` (i.e., the filter containing all powersets of members of `lb`), with respect to a filter `la` on `α`, if and only if for every set `t` in `lb`, there is an 'eventually' condition in `la` such that for all `x` of type `α`, `g(x)` is a subset of `t`. Here, 'eventually' refers to the property that the condition holds for all `x` in the filter `la` from some point forward.
More concisely: A function `g` from type `α` to sets of type `β` converges to the filter `lb` with respect to filter `la` if and only if for every set `t` in `lb`, there exists an eventually true condition in `la` such that for all `x` in `α`, `g(x)` is a subset of `t`.
|
Filter.eventually_smallSets_eventually
theorem Filter.eventually_smallSets_eventually :
∀ {α : Type u_1} {l l' : Filter α} {p : α → Prop},
(∀ᶠ (s : Set α) in l.smallSets, ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x
The theorem `Filter.eventually_smallSets_eventually` states that for any two filters `l` and `l'` over some type `α`, and a property `p` of type `α → Prop`, the condition that all sets `s` eventually in the filter of small sets of `l` have the property that all elements `x` eventually in `l'` and belonging to `s` satisfy `p`, is equivalent to the condition that all elements `x` eventually in the infimum of filters `l` and `l'` satisfy `p`. In other words, it relates the eventual satisfaction of a property in a filter and its small sets filter.
More concisely: For filters `l` and `l'` over type `α` and property `p`, the filter `l` has only eventually small sets with property `p` if and only if the infimum of `l` and `l'` has all its elements eventually satisfying `p`.
|
Filter.eventually_smallSets
theorem Filter.eventually_smallSets :
∀ {α : Type u_1} {l : Filter α} {p : Set α → Prop}, (∀ᶠ (s : Set α) in l.smallSets, p s) ↔ ∃ s ∈ l, ∀ t ⊆ s, p t
The theorem `Filter.eventually_smallSets` states that, for any type `α`, any filter `l` on `α`, and any property `p` that sets of `α` might have, the statement "For almost all (in the sense of the filter `Filter.smallSets l`) sets `s` of `α`, the property `p` holds for `s`" is equivalent to the statement "There exists a set `s` in the filter `l` such that for all subsets `t` of `s`, the property `p` holds for `t`." Essentially, it provides a condition for a property to hold almost everywhere with respect to the `smallSets` filter of a given filter.
More concisely: For any filter `l` on type `α` and property `p` on sets of `α`, the property "almost all sets in the filter `l` satisfy `p`" is equivalent to "there exists a set in `l` whose every subset satisfies `p`."
|
Filter.eventually_smallSets'
theorem Filter.eventually_smallSets' :
∀ {α : Type u_1} {l : Filter α} {p : Set α → Prop},
(∀ ⦃s t : Set α⦄, s ⊆ t → p t → p s) → ((∀ᶠ (s : Set α) in l.smallSets, p s) ↔ ∃ s ∈ l, p s)
The theorem `Filter.eventually_smallSets'` states that for any type `α`, any filter `l` of `α`, and any property `p` that sets of `α` might have, if `p` is monotonic (meaning that whenever set `s` is a subset of set `t` and `t` has property `p`, then `s` also has property `p`), then `p` holds eventually for the small sets in filter `l` if and only if there exists a set `s` in `l` such that `s` has property `p`. Here, "eventually" means that there are only finitely many exceptions, and "small sets in filter `l`" refers to the sets that are in the largest filter containing all powersets of members of `l`.
More concisely: For any filter `l` on type `α`, property `p` monotonic on sets, if and only if every set in the filter of small sets of `l` having property `p` is non-empty, then `p` holds eventually for all sets in `l`.
|
Filter.Eventually.of_smallSets
theorem Filter.Eventually.of_smallSets :
∀ {α : Type u_1} {l : Filter α} {p : α → Prop},
(∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) → ∀ᶠ (x : α) in l, p x
The theorem `Filter.Eventually.of_smallSets` states that for any type `α`, any filter `l` on `α`, and any property `p` that an element of `α` can satisfy, if every element of every set `s` in the collection of small sets of the filter `l` satisfies the property `p` (i.e., for all `s` in `l.smallSets`, for all `x` in `s`, `p x` holds), then every element that eventually appears in the filter `l` will satisfy the property `p` (i.e., for all `x` in `l`, `p x` holds). In other words, if a property holds for all elements of all small sets of a filter, then the property eventually holds for all elements of the filter.
More concisely: If every small set in a filter satisfies a property, then every element eventually in the filter also satisfies that property.
|
Filter.smallSets_bot
theorem Filter.smallSets_bot : ∀ {α : Type u_1}, ⊥.smallSets = pure ∅
The theorem `Filter.smallSets_bot` states that for any type `α`, the filter `smallSets` applied to the bottom filter (notated as `⊥`, which is the smallest filter or the trivial filter that only contains the whole set) is equal to the pure filter of the empty set. In other words, the largest filter containing all powersets of members of the smallest filter in a given type is the pure filter of the empty set.
More concisely: For any type α, the filter of small sets applied to the bottom filter is equal to the pure filter of the empty set.
|
Filter.Eventually.smallSets
theorem Filter.Eventually.smallSets :
∀ {α : Type u_1} {l : Filter α} {p : α → Prop},
(∀ᶠ (x : α) in l, p x) → ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x
This theorem, referred to as an alias of the reverse direction of `Filter.eventually_smallSets_forall`, states the following: for any type `α`, any filter `l` on `α`, and any property `p` of elements of `α`, if `p` holds eventually (that is, for all elements in some subset) in the filter `l`, then `p` holds for all elements `x` in all sets `s` that eventually appear in the collection of small sets of the filter `l`.
More concisely: If a property holds eventually in a filter, then it holds for all elements in all small sets that eventually appear in the filter.
|