ZeroAtInftyContinuousMap.coe_add
theorem ZeroAtInftyContinuousMap.coe_add :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddZeroClass β]
[inst_3 : ContinuousAdd β] (f g : ZeroAtInftyContinuousMap α β), ⇑(f + g) = ⇑f + ⇑g
This theorem states that for any two continuous functions 'f' and 'g' from one topological space 'α' to another 'β' (where 'β' has a zero and an addition operation, and the addition operation is continuous), the addition of the functions 'f' and 'g' (which gives another continuous function from 'α' to 'β') behaves as expected: applying this sum function to an input is the same as separately applying 'f' and 'g' to that input and then adding the results. This is to say, for these continuous functions, addition is preserved under the function application operation.
More concisely: For any continuous functions $f, g : X \rightarrow Y$ from a topological space $X$ to a topological group $Y$ with a continuous addition operation, the function $h : X \rightarrow Y$ defined by $h(x) = f(x) + g(x)$ is continuous, and for all $x \in X$, $h(x) = f(x) + g(x) = f(x) + g(x)$.
|
ZeroAtInftyContinuousMap.tendsto_iff_tendstoUniformly
theorem ZeroAtInftyContinuousMap.tendsto_iff_tendstoUniformly :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
{ι : Type u_2} {F : ι → ZeroAtInftyContinuousMap α β} {f : ZeroAtInftyContinuousMap α β} {l : Filter ι},
Filter.Tendsto F l (nhds f) ↔ TendstoUniformly (fun i => ⇑(F i)) (⇑f) l
This theorem states that for any topological space `α`, pseudometric space `β` with a zero element, a type `ι`, a sequence of continuous maps `F` from `ι` to the set of continuous functions from `α` to `β` that vanish at infinity, a limiting continuous function `f` that also vanishes at infinity, and a filter `l` on `ι`, the sequence `F` converges to `f` with respect to the filter `l` in the metric on the space of continuous functions that vanish at infinity (`C₀(α, β)`) if and only if `F` converges uniformly to `f` with respect to the filter `l`. The 'uniform convergence' here means that for any entourage of the diagonal in the uniform space `β`, eventually for all `ι` in the filter `l`, the pair `(f x, Fₙ x)` belongs to the entourage for all `x` in `α`. The 'convergence in the metric on `C₀(α, β)`' means that for every neighborhood of `f`, the preimage of this neighborhood under `F` is a neighborhood in the filter `l`.
More concisely: For any topological space α, pseudometric space β with a zero element, type ι, sequence of continuous functions F from ι to the space of continuous functions from α to β that vanish at infinity, limiting continuous function f that also vanishes at infinity, and filter l on ι, F converges to f uniformly with respect to the diagonal metric on β if and only if F converges to f in the metric on C₀(α, β) with respect to the filter l.
|
ZeroAtInftyContinuousMap.coe_mul
theorem ZeroAtInftyContinuousMap.coe_mul :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : MulZeroClass β]
[inst_3 : ContinuousMul β] (f g : ZeroAtInftyContinuousMap α β), ⇑(f * g) = ⇑f * ⇑g
This theorem states that for any two objects `f` and `g` of type `ZeroAtInftyContinuousMap` (which map a topological space `α` to another `β` where `β` is a `MulZeroClass`, i.e., a class where multiplication by zero yields zero and has a notion of multiplication), the operation of pointwise multiplication on the co-domain (`β`) commutes with the operation of taking the coercion (i.e., the actual function) of the continuous map. In other words, taking the product of the two maps `f` and `g` and then applying the resultant map to a point is the same as applying `f` and `g` to the point separately and then taking the product in `β`. Here, `β` is assumed to also have a topological structure that makes multiplication a continuous operation.
More concisely: For any `f : α → ZeroAtInftyContinuousMap β` and `g : α → ZeroAtInftyContinuousMap β` where `β` is a `MulZeroClass` with a continuous multiplication, the diagram commutes: `(f ⊤) ⊤ * (g ⊤) ⊤ = (f ⊤ * g ⊤) ⊤`, where `⊤` denotes the coercion from `ZeroAtInftyContinuousMap β` to `β`.
|
ZeroAtInftyContinuousMapClass.zero_at_infty
theorem ZeroAtInftyContinuousMapClass.zero_at_infty :
∀ {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} [inst : TopologicalSpace α] [inst_1 : Zero β]
[inst_2 : TopologicalSpace β] [inst_3 : FunLike F α β] [self : ZeroAtInftyContinuousMapClass F α β] (f : F),
Filter.Tendsto (⇑f) (Filter.cocompact α) (nhds 0)
The theorem `ZeroAtInftyContinuousMapClass.zero_at_infty` states that for any member `f` of a class `F` which is a function-like object from a topological space `α` to a topological space `β` with zero element, the function `f` tends to zero along the `cocompact` filter of `α`. Here, the `cocompact` filter on a topological space is the filter generated by the complements of compact sets, and `nhds 0` denotes the neighborhood filter of the zero element in `β`. This theorem essentially shows that "at infinity", each member of the class `F` goes to zero.
More concisely: For any continuous function-like object `f` from a topological space `α` to a topological space `β` with zero element, `f` tends to zero in the limit along the cocompact filter of `α`, i.e., for every neighborhood `U` of the zero element in `β`, there exists a compact set `K` in `α` such that `f(x)` is in `U` for all `x` in the complement of `K`.
|
ZeroAtInftyContinuousMap.coe_neg
theorem ZeroAtInftyContinuousMap.coe_neg :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
[inst_3 : TopologicalAddGroup β] (f : ZeroAtInftyContinuousMap α β), ⇑(-f) = -⇑f
This theorem states that for any zero-at-infinity continuous map `f` from a topological space `α` to a topological add group `β`, applying the negation operation to `f` and then applying the result to an element is the same as applying `f` to the element and then applying the negation operation. In other words, the negation operation commutes with the application of the zero-at-infinity continuous map.
More concisely: For any zero-at-infinity continuous map `f` from a topological space `α` to a topological add group `β`, we have `- (f (x)) = f (-x)` for all `x` in `α`.
|
ZeroAtInftyContinuousMap.coe_zero
theorem ZeroAtInftyContinuousMap.coe_zero :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β], ⇑0 = 0
This theorem states that for any types `α` and `β`, where `α` and `β` both have topological space structures and `β` has a zero element, the continuous map at infinity (denoted by `⇑0`) is equal to the zero element of `β`. In other words, in this context, the map that sends all elements of `α` to the zero of `β` is equivalent to the zero function.
More concisely: For any topological spaces `α` and `β` with a zero element in `β`, the continuous map from `α` to `β` sending all elements to the zero element is the zero function.
|
ZeroAtInftyContinuousMap.ext
theorem ZeroAtInftyContinuousMap.ext :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
{f g : ZeroAtInftyContinuousMap α β}, (∀ (x : α), f x = g x) → f = g
This theorem states that for any two continuous maps `f` and `g` from a topological space `α` to another topological space `β` that is also a zero space, if `f` and `g` are equal at every point in `α`, then `f` and `g` are the same continuous map. In other words, two continuous maps from `α` to `β` are identical if and only if they have the same value at every point in `α`.
More concisely: Two continuous functions from a topological space to a zero space are equal if and only if they agree at every point.
|
ZeroAtInftyContinuousMap.coe_sub
theorem ZeroAtInftyContinuousMap.coe_sub :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
[inst_3 : TopologicalAddGroup β] (f g : ZeroAtInftyContinuousMap α β), ⇑(f - g) = ⇑f - ⇑g
This theorem states that for any two continuous maps 'f' and 'g' from a topological space 'α' to a topological add group 'β' that vanish at infinity, the mapping of the difference between 'f' and 'g' is equal to the difference of the individual mappings of 'f' and 'g'. Here, 'β' is not just a topological space but also an additive group, and the addition operation is continuous.
More concisely: For continuous functions $f, g : \alpha \to (\beta, +)$ with $\beta$ being a topological add group and $f, g$ vanishing at infinity, we have $f - g : \alpha \to \beta$ being the continuous function equal to $f - g : \alpha \to \beta$ defined pointwise.
|
ZeroAtInftyContinuousMap.zero_at_infty'
theorem ZeroAtInftyContinuousMap.zero_at_infty' :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
(self : ZeroAtInftyContinuousMap α β), Filter.Tendsto self.toFun (Filter.cocompact α) (nhds 0)
The theorem `ZeroAtInftyContinuousMap.zero_at_infty'` asserts that for every type `α` with a topology and every type `β` that has a topology and a zero element, for every instance of `ZeroAtInftyContinuousMap` from `α` to `β`, the function defined by this instance tends to zero along the `cocompact` filter of `α`. In other words, for every neighborhood of zero in `β`, the pre-image under this function of the neighborhood is a neighborhood in the `cocompact` filter of `α`. The `cocompact` filter of a type with a topology is generated by the complements of its compact sets.
More concisely: For every continuous function from a topological space with a compact exhaustion to a space with a zero element, the function tends to zero along the cocompact filter.
|