Filter.Tendsto.Icc
theorem Filter.Tendsto.Icc :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {l₁ l₂ : Filter α}
[inst_1 : Filter.TendstoIxxClass Set.Icc l₁ l₂] {lb : Filter β} {u₁ u₂ : β → α},
Filter.Tendsto u₁ lb l₁ →
Filter.Tendsto u₂ lb l₁ → Filter.Tendsto (fun x => Set.Icc (u₁ x) (u₂ x)) lb l₂.smallSets
The theorem `Filter.Tendsto.Icc` states that for any types `α` and `β`, with `α` having a preorder structure, any filters `l₁` and `l₂` on `α`, and any functions `u₁` and `u₂` from `β` to `α`, if we have `Filter.Tendsto u₁ lb l₁` and `Filter.Tendsto u₂ lb l₁`, i.e., the functions `u₁` and `u₂` tend to filters `l₁` as the input points tend to filter `lb`, then the function that maps `x` to the closed interval `[u₁(x), u₂(x)]` also tends to the filter of small sets of `l₂` as `x` tends to filter `lb`. Here, `Filter.TendstoIxxClass Set.Icc l₁ l₂` is an assumption that the interval function `Set.Icc` tends from `l₁` to `l₂`, and `Filter.smallSets l₂` represents the largest filter containing all powersets of members of `l₂`.
More concisely: For filters `l₁` and `l₂` on a preordered type `α`, and functions `u₁` and `u₂` from a type `β` to `α`, if `u₁` and `u₂` tend to filters `l₁` and `l₁` is contained in the domain of convergence of `Set.Icc` with respect to `l₂`, then the function that maps `x` to the closed interval `[u₁(x), u₂(x)]` tends to the filter of small sets of `l₂`.
|
Filter.tendstoIxxClass_of_subset
theorem Filter.tendstoIxxClass_of_subset :
∀ {α : Type u_1} {l₁ l₂ : Filter α} {Ixx Ixx' : α → α → Set α},
(∀ (a b : α), Ixx a b ⊆ Ixx' a b) →
∀ [h' : Filter.TendstoIxxClass Ixx' l₁ l₂], Filter.TendstoIxxClass Ixx l₁ l₂
The theorem `Filter.tendstoIxxClass_of_subset` states that for any given type `α` and any two filters `l₁` and `l₂` on this type, if we have two operations `Ixx` and `Ixx'` from `α` to `α` to `Set α` such that for every pair of elements `(a, b)` from `α`, `Ixx a b` is a subset of `Ixx' a b`, then if `Ixx'` is a TendstoIxxClass from `l₁` to `l₂`, it follows that `Ixx` is also a TendstoIxxClass from `l₁` to `l₂`.
In other words, this theorem says that if one operation between elements of a type that results in a set is always a subset of another operation, and if the second operation gives us a TendstoIxxClass (a certain kind of mapping from one filter to another), then the first operation will also give us a TendstoIxxClass.
More concisely: Given filters `l₁` and `l₂` on type `α`, if operation `Ixx'` is a TendstoIxxClass from `l₁` to `l₂` and for all `a, b ∈ α`, `Ixx a b` is a subset of `Ixx' a b`, then `Ixx` is also a TendstoIxxClass from `l₁` to `l₂`.
|
Filter.HasBasis.tendstoIxxClass
theorem Filter.HasBasis.tendstoIxxClass :
∀ {α : Type u_1} {ι : Type u_3} {p : ι → Prop} {s : ι → Set α} {l : Filter α},
l.HasBasis p s →
∀ {Ixx : α → α → Set α},
(∀ (i : ι), p i → ∀ x ∈ s i, ∀ y ∈ s i, Ixx x y ⊆ s i) → Filter.TendstoIxxClass Ixx l l
The theorem `Filter.HasBasis.tendstoIxxClass` states that for any type `α` and an index type `ι`, given a predicate `p` on `ι`, a map `s` from `ι` to a set of `α`, and a filter `l` on `α`, if the filter `l` has a basis characterized by the predicate `p` and the map `s`, then for any index set function `Ixx`, if for every `i` in `ι` where the predicate `p` holds, every pair of elements `x` and `y` from the set `s i` satisfies that `Ixx x y` is a subset of `s i`, then the filter `l` tends to the Ixx class defined by `Ixx`. In simpler words, it describes a condition under which a filter has a certain "tendency" property with respect to an index set function.
More concisely: If a filter on a set, indexed by a type, has a basis characterized by a predicate and a map, and the map images satisfy a certain condition with respect to an index set function, then the filter tends to the Ixx class defined by the function.
|
Filter.TendstoIxxClass.tendsto_Ixx
theorem Filter.TendstoIxxClass.tendsto_Ixx :
∀ {α : Type u_1} {Ixx : α → α → Set α} {l₁ : Filter α} {l₂ : outParam (Filter α)}
[self : Filter.TendstoIxxClass Ixx l₁ l₂],
Filter.Tendsto (fun p => Ixx p.1 p.2) (l₁ ×ˢ l₁) (Filter.smallSets l₂)
This theorem states that for any given types `α`, any function `Ixx` which maps two elements of `α` to a set of `α`, any filters `l₁` and `l₂` on `α`, and any instance of `Filter.TendstoIxxClass` of `Ixx`, `l₁`, and `l₂`, the function `uncurry Ixx` has the property of tending to `l₂.smallSets` along the filter `l₁ ×ˢ l₁`. This means that for any set `s` in `l₂`, there exists a set `t` in `l₁` such that the image of every pair `(x, y)` from `t` under `Ixx` is a subset of `s`. This theorem suggests using lemmas like `Filter.Tendsto.Icc` instead.
More concisely: For any type `α`, function `Ixx` mapping pairs of `α` to sets, filters `l₁` and `l₂` on `α`, and instance of `Filter.TendstoIxxClass` for `Ixx`, `l₁`, and `l₂`, the function `uncurry Ixx` tends to `l₂.smallSets` along the product filter `l₁ ×ˢ l₁`.
|
Filter.tendstoIxxClass_principal
theorem Filter.tendstoIxxClass_principal :
∀ {α : Type u_1} {s t : Set α} {Ixx : α → α → Set α},
Filter.TendstoIxxClass Ixx (Filter.principal s) (Filter.principal t) ↔ ∀ x ∈ s, ∀ y ∈ s, Ixx x y ⊆ t
This theorem, `Filter.tendstoIxxClass_principal`, states that for any type `α`, and for any sets `s` and `t` of type `α`, and for any function `Ixx` that takes two elements of type `α` and returns a set of type `α`, the function `Ixx` has the property of TendstoIxxClass between the principal filter of `s` and the principal filter of `t` if and only if for all elements `x` and `y` in set `s`, all elements in the set `Ixx x y` are also in set `t`. Here, `TendstoIxxClass` represents a certain kind of "limiting behavior" of the function `Ixx`, specifically, it pertains to how the function `Ixx` behaves for values in `s` tending towards values in `t`.
More concisely: For any function `Ixx` from a type `α` to sets of `α`, `Filter.tendstoIxxClass_principal` states that `Ixx` tends to the principal filters of `s` and `t` if and only if for all `x, y in s`, every element in `Ixx x y` is in `t`.
|