Mathlib.Topology.Order.Lattice._auxLemma.2
theorem Mathlib.Topology.Order.Lattice._auxLemma.2 :
∀ {α : Type u_2} {β : Type u_3} {C : β → Type u_7} [inst : (b : β) → SemilatticeSup (C b)]
[inst_1 : (b : β) → OrderBot (C b)] (s : Finset α) (f : α → (b : β) → C b) (b : β),
(s.sup fun a => f a b) = s.sup f b
This theorem states that for any types `α`, `β` and function `C : β → Type`, given a semilattice structure and an order bot structure on `C b` for each `b : β`, a finite set `s : Finset α`, a function `f : α → (b : β) → C b`, and an element `b : β`, the supremum of the set of values `f a b` (where `a` is an element of `s`) is equal to the supremum of the set of values `f b` (where `f` is applied to each element of `s`).
In simpler terms, it says that the order of applying the function `f` and taking the supremum does not matter: we can either first apply `f` to each element of the set and then take the supremum, or take the supremum first and then apply `f`. This can be thought of as a kind of "commutativity property" of the supremum computation with respect to function application.
More concisely: For any semilattice `C` with order bot structures on `C b` for each `b`, given a finite set `s`, function `f : α → β → C`, and `b : β`, the supremum of `{f a b | a ∈ s}` is equal to the supremum of `{f b | b ∈ set.image b s}` (where `set.image b s` is the image of `s` under the function `b`).
|
Filter.Tendsto.inf_nhds'
theorem Filter.Tendsto.inf_nhds' :
∀ {L : Type u_1} [inst : TopologicalSpace L] {α : Type u_3} {l : Filter α} {f g : α → L} {x y : L} [inst_1 : Inf L]
[inst_2 : ContinuousInf L],
Filter.Tendsto f l (nhds x) → Filter.Tendsto g l (nhds y) → Filter.Tendsto (f ⊓ g) l (nhds (x ⊓ y))
The theorem `Filter.Tendsto.inf_nhds'` is a statement about the limit behavior of two functions `f` and `g` in a topological space `L` equipped with an infimum operation (denoted as "⊓") and where the infimum operation is continuous. If the limit of function `f` along a filter `l` tends to a neighborhood of a point `x` and the limit of function `g` along the same filter `l` tends to a neighborhood of point `y`, then the limit of the infimum of functions `f` and `g` (i.e., `(f ⊓ g)`) also along the filter `l` tends to the neighborhood of the infimum of the points `x` and `y` (i.e., `(x ⊓ y)`). In other words, it establishes that the limit of the infimum of two functions is the infimum of their limits when those limits are in a neighborhood filter and the infimum operation is continuous.
More concisely: If functions `f` and `g` have limit values `x` and `y` in a topologically complete space `L` equipped with a continuous infimum operation, then the limit of the infimum `(f ⊓ g)` along any filter `l` tends to the infimum `(x ⊓ y)` in `L`.
|
Filter.Tendsto.finset_sup'_nhds
theorem Filter.Tendsto.finset_sup'_nhds :
∀ {L : Type u_1} [inst : TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ι → α → L}
{l : Filter α} {g : ι → L} [inst_1 : SemilatticeSup L] [inst_2 : ContinuousSup L] (hne : s.Nonempty),
(∀ i ∈ s, Filter.Tendsto (f i) l (nhds (g i))) → Filter.Tendsto (s.sup' hne f) l (nhds (s.sup' hne g))
This theorem states that in a topological space `L` which is a join-semilattice and allows for a continuous supremum operation, for any nonempty finite set `s` and any filter `l` on `α`, if for each element `i` in `s`, the function `f i` tends from filter `l` to the neighborhood of `g i`, then the supremum of the images of `s` under `f` tends from filter `l` towards the neighborhood of the supremum of the images of `s` under `g`.
More concisely: In a topological space endowed with a continuous supremum operation, if for each element of a finite set and for any filter, the functions map the set to neighborhoods of their respective images under another function, then the supremum of the functions' images under the first function tends to the supremum of their images under the second function as the filter approaches its limit.
|
Filter.Tendsto.sup_nhds
theorem Filter.Tendsto.sup_nhds :
∀ {L : Type u_1} [inst : TopologicalSpace L] {α : Type u_3} {l : Filter α} {f g : α → L} {x y : L} [inst_1 : Sup L]
[inst_2 : ContinuousSup L],
Filter.Tendsto f l (nhds x) →
Filter.Tendsto g l (nhds y) → Filter.Tendsto (fun i => f i ⊔ g i) l (nhds (x ⊔ y))
This theorem states that for any type `L` that is a topological space and equipped with an operation `⊔` (supremum), and for any functions `f` and `g` from a type `α` to `L`, if `f` tends to `x` and `g` tends to `y` with respect to a filter `l` (i.e., as we take values from `l`, `f` gets closer to `x` and `g` gets closer to `y`), then the function which for each input `i` in `α` takes the supremum of `f(i)` and `g(i)` also tends towards the supremum of `x` and `y` with respect to the same filter `l`. This holds under the condition that `L` is a continuous sup space, meaning that the supremum operation is continuous.
More concisely: Let `(L, ⊔)` be a continuous sup space, and given functions `f, g: α -> L` from a type `α` to `L`, if `f` converges to `x` and `g` converges to `y` with respect to a filter `l`, then the function `i => ⊔(f i, g i)` converges to `⊔(x, y)` with respect to `l`.
|
Filter.Tendsto.finset_sup'_nhds_apply
theorem Filter.Tendsto.finset_sup'_nhds_apply :
∀ {L : Type u_1} [inst : TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ι → α → L}
{l : Filter α} {g : ι → L} [inst_1 : SemilatticeSup L] [inst_2 : ContinuousSup L] (hne : s.Nonempty),
(∀ i ∈ s, Filter.Tendsto (f i) l (nhds (g i))) →
Filter.Tendsto (fun a => s.sup' hne fun x => f x a) l (nhds (s.sup' hne g))
This theorem states that if we have a topological space `L` with a structure of a join-semilattice (a type of partially ordered set) and where the supremum operation is continuous, a nonempty finite set `s`, a filter `l` on `α`, and a function `f : ι → α → L` that tends to a function `g : ι → L` at each point of `s`, then the function `h : α → L` that maps each `α` to the supremum of the image of `s` under `f` also tends to the supremum of the image of `s` under `g` as `α` varies under the filter `l`. In other words, if each `f i` approaches `g i` for `i` in `s`, then the supremum of the `f i`'s also approaches the supremum of the `g i`'s.
More concisely: If `L` is a topological space with a continuous supremum operation, `s` is a nonempty finite set, `l` is a filter on `α`, and `f : ι → α → L` tends to `g : ι → L` at each point of `s`, then the function `h(x) = sup(fi(x))_s` tends to `sup(gi(x))_s` as `x` varies under the filter `l`.
|
Filter.Tendsto.finset_sup_nhds_apply
theorem Filter.Tendsto.finset_sup_nhds_apply :
∀ {L : Type u_1} [inst : TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ι → α → L}
{l : Filter α} {g : ι → L} [inst_1 : SemilatticeSup L] [inst_2 : OrderBot L] [inst_3 : ContinuousSup L],
(∀ i ∈ s, Filter.Tendsto (f i) l (nhds (g i))) →
Filter.Tendsto (fun a => s.sup fun x => f x a) l (nhds (s.sup g))
This theorem states that for a given topological space `L`, a finset `s` with elements of type `ι`, a function `f` mapping `ι` to a function from `α` to `L`, a filter `l` over `α`, a function `g` mapping `ι` to `L`, if `L` is equipped with a semilattice structure, a bottom element, and a continuity property for the supremum operation, then if for each element `i` in `s`, the function `f i` tends to the neighborhood filter of `g i` under the filter `l`, then the function that takes an element of `α` and maps it to the supremum of the set `{f x a | x ∈ s}` also tends to the neighborhood filter of the supremum of the set `{g x | x ∈ s}` under the filter `l`.
The theorem is about the convergence of a function mapping to the supremum of a set of functions within a topological space that has a semilattice structure with a bottom element and a continuous supremum operation. It essentially says that if each individual function in the set converges to a point, then the function mapping to the supremum of these functions also converges to the supremum of these points.
More concisely: Given a topological space equipped with a semilattice structure, a bottom element, and continuous supremum operation, if for each element in a finite set and corresponding functions from the set to the space, the functions converge to their respective neighborhood filters under a filter, then the function mapping each element to the supremum of the set of functions for that element converges to the supremum of the neighborhood filters under the filter.
|
ContinuousSup.continuous_sup
theorem ContinuousSup.continuous_sup :
∀ {L : Type u_1} [inst : TopologicalSpace L] [inst_1 : Sup L] [self : ContinuousSup L],
Continuous fun p => p.1 ⊔ p.2
This theorem states that the supremum function, which gets a pair of elements and returns their supremum, is continuous for any type `L`. The type `L` should be equipped with a topology, meaning it has a defined notion of 'closeness' or 'continuity', and it should have a defined supremum operation. This is under the condition that the supremum operation is continuous in the topological space `L`, which is indicated by the presence of the `ContinuousSup L` instance. In other words, small changes in the input of the supremum function result in small changes in its output.
More concisely: If `L` is a topological space with a continuous supremum operation, then the supremum function is a continuous function on `L x L`.
|
ContinuousInf.continuous_inf
theorem ContinuousInf.continuous_inf :
∀ {L : Type u_1} [inst : TopologicalSpace L] [inst_1 : Inf L] [self : ContinuousInf L],
Continuous fun p => p.1 ⊓ p.2
The theorem `ContinuousInf.continuous_inf` states that for any type `L` that has a topological space structure, an infimum operation, and also the property of being a continuous infimum, the operation that takes a pair `p` of elements from `L` and returns their infimum (`p.1 ⊓ p.2`) is a continuous function. In other words, the infimum operation preserves the topological structure of `L`.
More concisely: For any topological space `L` with a continuous infimum operation, the function `λ p : L × L, p.1 ⊓ p.2` is continuous.
|
Continuous.inf
theorem Continuous.inf :
∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Inf L]
[inst_3 : ContinuousInf L] {f g : X → L}, Continuous f → Continuous g → Continuous fun x => f x ⊓ g x
This theorem states that for any types `L` and `X`, where `L` is a topological space with an infimum operation and `X` is another topological space, if we have two continuous functions `f` and `g` from `X` to `L`, then the function that maps each point in `X` to the infimum of the images of that point under `f` and `g` is also a continuous function. This theorem captures the property that the infimum operation is continuous in topological spaces.
More concisely: Given topological spaces `L` with an infimum operation and `X`, if `f` and `g` are continuous functions from `X` to `L`, then the function mapping each point in `X` to the infimum of `f(x)` and `g(x)` is also continuous.
|
Filter.Tendsto.sup_nhds'
theorem Filter.Tendsto.sup_nhds' :
∀ {L : Type u_1} [inst : TopologicalSpace L] {α : Type u_3} {l : Filter α} {f g : α → L} {x y : L} [inst_1 : Sup L]
[inst_2 : ContinuousSup L],
Filter.Tendsto f l (nhds x) → Filter.Tendsto g l (nhds y) → Filter.Tendsto (f ⊔ g) l (nhds (x ⊔ y))
This theorem states that for any two functions `f` and `g` mapping from a generic type `α` to a topological space `L`, and given that the type `L` supports a supremum operation (denoted by `⊔`) and that this supremum operation is continuous, if `f` tends to a neighborhood of a point `x` and `g` tends to a neighborhood of a point `y` (with respect to some filter `l`), then the function that maps each point in the domain to the supremum of the images of `f` and `g` at that point also tends towards the neighborhood of the supremum of `x` and `y`. In mathematical terms, if $\lim_{l} f = x$ and $\lim_{l} g = y$, then $\lim_{l} (f ⊔ g) = x ⊔ y$.
More concisely: Given functions `f` and `g` from type `α` to a topological space `L` with a continuous supremum operation, if `f` converges to `x` and `g` converges to `y` (with respect to some filter) then `f ⊔ g` converges to `x ⊔ y`.
|
Continuous.sup
theorem Continuous.sup :
∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Sup L]
[inst_3 : ContinuousSup L] {f g : X → L}, Continuous f → Continuous g → Continuous fun x => f x ⊔ g x
This theorem states that for any two functions `f` and `g` from a topological space `X` to another topological space `L` with a supremum operation `⊔` and continuity of this operation, if both `f` and `g` are continuous, then the function that maps each point `x` in the domain to the supremum of `f(x)` and `g(x)` is also continuous. This is a property of continuous functions in a topological space that have a supremum operation.
More concisely: If `f` and `g` are continuous functions from a topological space `X` to a topological space `L` with a supremum operation `⊔`, then the function `x ↦ ⊔(f(x), g(x))` is also continuous.
|
Mathlib.Topology.Order.Lattice._auxLemma.1
theorem Mathlib.Topology.Order.Lattice._auxLemma.1 :
∀ {α : Type u_2} {β : Type u_3} {C : β → Type u_7} [inst : (b : β) → SemilatticeSup (C b)] {s : Finset α}
(H : s.Nonempty) (f : α → (b : β) → C b) (b : β), (s.sup' H fun a => f a b) = s.sup' H f b
This theorem states that for any types `α`, `β`, and a type family `C : β → Type`, where each `C b` forms a join-semilattice, along with a nonempty finite set `s` of type `α`, a function `f : α → (b : β) → C b`, and any `b : β`, the supremum of the images of elements in `s` under the function `(λa, f a b)` is equal to the supremum of the images of elements in `s` under the function `f` evaluated at `b`. In other words, the order of applying the function `f` and taking the supremum does not matter.
More concisely: For any type families `C : β → Type` forming join-semilattices, type `α`, finite nonempty set `s : α`, function `f : α → β → C β`, and `b : β`, the image of the supremum of `s` under `λa, f a b` is equal to the supremum of the images of elements in `s` under `f` at `b`.
|
continuous_sup
theorem continuous_sup :
∀ {L : Type u_1} [inst : TopologicalSpace L] [inst_1 : Sup L] [inst_2 : ContinuousSup L],
Continuous fun p => p.1 ⊔ p.2
This theorem states that for any type `L` that has a topological space structure, a sup (supremum) operation, and for which the sup operation is continuous, the function that takes a pair of elements in `L` and returns their supremum is a continuous function. In mathematical terms, if we have a topological space `L` with a defined supremum operation that is continuous, then the map `(x, y) -> x ⊔ y` is a continuous map.
More concisely: If `(L, �intersection, ∪, ∅, ∏, ⊤, ⊥, ≤)` is a complete lattice in a topological space with a continuous supremum operation, then the function `(x, y) ↦ x ⊔ y` is continuous.
|
continuous_inf
theorem continuous_inf :
∀ {L : Type u_1} [inst : TopologicalSpace L] [inst_1 : Inf L] [inst_2 : ContinuousInf L],
Continuous fun p => p.1 ⊓ p.2
This theorem states that for any type `L` that is equipped with a topology (i.e., `L` is a topological space) and has an infimum operation (denoted by `⊓`), if the infimum operation is continuous, then the function that takes a pair `p` of elements from `L` and returns their infimum `p.1 ⊓ p.2` is also continuous. In other words, if `L` is a topological space where the "greatest lower bound" operation is continuous, then applying this operation to any pair of elements is a continuous operation.
More concisely: If `L` is a topological space with a continuous infimum operation, then the function `λ p: L × L, p.1 ⊓ p.2` is continuous from `L × L` to `L`.
|