Filter.le_pi
theorem Filter.le_pi :
∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {g : Filter ((i : ι) → α i)},
g ≤ Filter.pi f ↔ ∀ (i : ι), Filter.Tendsto (Function.eval i) g (f i)
The theorem `Filter.le_pi` states that for any index type `ι`, any type function `α` indexed by `ι`, any family of filters `f` indexed by `ι`, and any filter `g` on the product type, the filter `g` is less than or equal to the product filter `π f` if and only if for every index `i` in `ι`, the function `Function.eval i` tends to the filter `f i` when taking `g` as the domain. In other words, this theorem characterizes when a filter `g` on the product type can be "lower-bounded" by a given product of filters, in terms of the convergence properties of the projections at each coordinate.
More concisely: For any index type `ι`, any type family `f : ι → Filter α`, and any filter `g : Filter (Π i, α i)`, `g ≤ ⨅ i, f i` if and only if `Function.eval i (g) ≤ f i` for all `i` in `ι`.
|
Filter.tendsto_pi
theorem Filter.tendsto_pi :
∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {β : Type u_3} {m : β → (i : ι) → α i}
{l : Filter β}, Filter.Tendsto m l (Filter.pi f) ↔ ∀ (i : ι), Filter.Tendsto (fun x => m x i) l (f i)
The theorem `Filter.tendsto_pi` states that for any type `ι`, a function `α` indexed by `ι`, a collection of filters `f` for each type `α i`, a type `β`, a function `m` mapping from `β` to each `α i`, and a filter `l` on `β`, the function `m` tends to the product of the filters `f` as defined by `Filter.pi` with respect to the filter `l` if and only if, for each `i` in `ι`, the function `m` applied to `i` tends to the corresponding filter `f i` with respect to the filter `l`. In other words, a function's limit with respect to a given filter is the product of the limits of the function applied to each element of the index set, each with respect to their corresponding filters.
More concisely: For any type `ι`, function `α → β`, filters `f` on `α i`, and filter `l` on `β`, the function `α → Filter β` given by `m ↦ Filter.pi f m` tends to `l` if and only if for all `i` in `ι`, the function `m i` tends to `f i` with respect to `l`.
|
Mathlib.Order.Filter.Pi._auxLemma.12
theorem Mathlib.Order.Filter.Pi._auxLemma.12 : ∀ {α : Type u} {f : Filter α}, f.NeBot = (f ≠ ⊥)
This theorem, `Mathlib.Order.Filter.Pi._auxLemma.12`, states that for any type `α` and any filter `f` of type `α`, the filter `f` is not a bottom filter if and only if `f` is not equal to the bottom filter. Here, `Filter.NeBot f` is a predicate indicating that `f` is a non-bottom (i.e., non-empty) filter, and `⊥` denotes the bottom filter. In the context of filter theory in mathematics, a bottom filter typically represents the empty set or a least element in a partially ordered set.
More concisely: A filter `f` of type `α` in Lean is not a bottom filter if and only if `f` is not equal to the bottom filter `⊥`.
|
Filter.tendsto_eval_pi
theorem Filter.tendsto_eval_pi :
∀ {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → Filter (α i)) (i : ι),
Filter.Tendsto (Function.eval i) (Filter.pi f) (f i)
The theorem `Filter.tendsto_eval_pi` asserts that for any indexed family of filters `(f : (i : ι) → Filter (α i))` and an index `i`, the function evaluation `Function.eval i` (which evaluates a function at the index `i`) is a limit function from the product filter `Filter.pi f` (which is the product of the indexed family of filters) to the filter `f i`. In simpler terms, when you apply a function to an element from the product of an indexed family of filters, the result will "tend to" or "converge to" the filter associated with the specific index used in the function evaluation.
More concisely: For any indexed family of filters `(f : (i : ι) → Filter (α i))`, the evaluation function `Function.eval : ∀ i, α i → α i` is a limit function from the product filter `Filter.pi f` to the filter `f i`.
|