ContinuousMap.hasSum_apply
theorem ContinuousMap.hasSum_apply :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {γ : Type u_3}
[inst_2 : AddCommMonoid β] [inst_3 : ContinuousAdd β] {f : γ → C(α, β)} {g : C(α, β)},
HasSum f g → ∀ (x : α), HasSum (fun i => (f i) x) (g x)
The theorem `ContinuousMap.hasSum_apply` states that for a locally compact topological space `α` and given any topological space `β`, if an infinite sum of functions from `C(α, β)` (the set of continuous functions from `α` to `β`) converges to a function `g` (with respect to the compact-open topology), then the sum, evaluated pointwise for any given `x` in `α`, converges to the value `g(x)`. Here, `HasSum f g` represents the property that the infinite sum of the sequence of functions `f` converges to `g`, and `HasSum (fun i => (f i) x) (g x)` represents that the infinite sum of the sequence `f i` evaluated at `x` converges to `g` evaluated at `x`.
More concisely: For any locally compact space α and topological space β, if (f\_n : α → β) is a sequence of continuous functions from α to β that converges to a function g with respect to the compact-open topology, then for all x in α, the sequence (f\_n x) converges to g x.
|
ContinuousMap.coe_pow
theorem ContinuousMap.coe_pow :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Monoid β]
[inst_3 : ContinuousMul β] (f : C(α, β)) (n : ℕ), ⇑(f ^ n) = ⇑f ^ n
This theorem states that for any types `α` and `β`, where `α` is a topological space and `β` is a topological space with a monoid structure and a continuous multiplication, given a continuous map `f` from `α` to `β` and a natural number `n`, the operation of applying the continuous map `f` `n` times (`f` to the power of `n`) is equivalent to applying the map `f` once and then taking the result to the power of `n`. In other words, the power operation commutes with the application of a continuous map.
More concisely: For any topological spaces `α` and `β` with `β` a monoid under a continuous multiplication, and for any continuous map `f : α → β` and natural number `n`, the map `f^n` is equivalent to the composition `(f ^ n) (x) = (f (x)) ^ n` for all `x ∈ α`.
|
ContinuousMap.coe_sub
theorem ContinuousMap.coe_sub :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Sub β]
[inst_3 : ContinuousSub β] (f g : C(α, β)), ⇑(f - g) = ⇑f - ⇑g
This theorem states that for any two continuous functions `f` and `g` from a topological space `α` to a topological space `β` (where `β` also has a subtraction operation and the subtraction operation is continuous), the pointwise subtraction of `f` and `g` is the same as the subtraction of the continuous maps `f` and `g`. In mathematical terms, for all `x` in `α`, `(f - g)(x) = f(x) - g(x)`.
More concisely: For any continuous functions `f` and `g` from a topological space `α` to a topological space `β` with a continuous subtraction operation, the pointwise subtraction `(f - g)(x)` equals the function subtraction `f(x) - g(x)` for all `x` in `α`.
|
ContinuousMap.coe_smul
theorem ContinuousMap.coe_smul :
∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
[inst_2 : SMul R M] [inst_3 : ContinuousConstSMul R M] (c : R) (f : C(α, M)), ⇑(c • f) = c • ⇑f
This theorem states that for any topological spaces `α` and `M`, a scalar multiplication operation `SMul` on `R` and `M`, and a continuity condition `ContinuousConstSMul` for this operation, the scalar multiplication of a continuous function `f` from `α` to `M` by a scalar `c` from `R` (`c • f`) is equivalent to the scalar multiplication of the function's output by `c` (`c • ⇑f`). In other words, scalar multiplication can be pulled outside of the function application.
More concisely: For any topological spaces `α`, `M`, continuous scalar multiplication operation `SMul` on `R` and `M`, and continuous function `f : α → M`, the scalar multiplication of `f` by a scalar `c` commutes with function application: `c • f = ⇑(c • SMul) ∘ f`.
|
ContinuousMap.compStarAlgHom'_id
theorem ContinuousMap.compStarAlgHom'_id :
∀ {X : Type u_1} [inst : TopologicalSpace X] (𝕜 : Type u_4) [inst_1 : CommSemiring 𝕜] (A : Type u_5)
[inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : TopologicalSemiring A] [inst_5 : Star A]
[inst_6 : ContinuousStar A] [inst_7 : Algebra 𝕜 A],
ContinuousMap.compStarAlgHom' 𝕜 A (ContinuousMap.id X) = StarAlgHom.id 𝕜 C(X, A)
The theorem `ContinuousMap.compStarAlgHom'_id` states that for any type `X` with a topological space structure, a type `𝕜` with a commutative semiring structure, and a type `A` with a topological space structure, semiring structure, topological semiring structure, star structure, continuous star structure, and algebra structure over `𝕜`, the composition of the identity continuous map (`ContinuousMap.id`) through the function `ContinuousMap.compStarAlgHom'` results in the identity Star algebra homomorphism (`StarAlgHom.id`), considering `𝕜` and the space of continuous maps from `X` to `A`, `C(X, A)`, as parameters. This essentially means that this function composition respects the identity function in the context of these mathematical structures.
More concisely: The theorem `ContinuousMap.compStarAlgHom'_id` asserts that the composition of the identity continuous map with `ContinuousMap.compStarAlgHom'` equals the identity star algebra homomorphism for any topological space `X`, semiring `𝕜`, and algebra `A` over `𝕜` with corresponding structures.
|
ContinuousMap.compStarAlgHom_id
theorem ContinuousMap.compStarAlgHom_id :
∀ (X : Type u_1) {𝕜 : Type u_2} {A : Type u_3} [inst : TopologicalSpace X] [inst_1 : CommSemiring 𝕜]
[inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : TopologicalSemiring A] [inst_5 : Star A]
[inst_6 : ContinuousStar A] [inst_7 : Algebra 𝕜 A],
ContinuousMap.compStarAlgHom X (StarAlgHom.id 𝕜 A) ⋯ = StarAlgHom.id 𝕜 C(X, A)
The theorem `ContinuousMap.compStarAlgHom_id` states that for any type `X` with a topological structure, any commutative semiring `𝕜`, any topological space `A` which also has a semiring structure and a star operation that is continuous, and for which `A` is an algebra over `𝕜`, the composition of the continuous map with the identity of the star algebra homomorphism on `A` is equal to the identity of the star algebra homomorphism on the space of continuous functions from `X` to `A`, denoted as `C(X, A)`.
More concisely: For any topological space X with a topology, commutative semiring ℝ, topological space A with a semiring and star operation structure, being an algebra over ℝ with a continuous star operation, the continuous map from X to A and the identity of the star algebra homomorphism on A commute, i.e., the composition is equal to the identity of the star algebra homomorphism on C(X, A).
|
ContinuousMap.coe_add
theorem ContinuousMap.coe_add :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Add β]
[inst_3 : ContinuousAdd β] (f g : C(α, β)), ⇑(f + g) = ⇑f + ⇑g
The theorem `ContinuousMap.coe_add` states that for any two continuous maps `f` and `g` from a topological space `α` to another topological space `β` (which also has an addition operation and where the addition operation is continuous), the pointwise addition of `f` and `g` is the same as their continuous sum. In other words, the coe function applied to the sum of `f` and `g` (`⇑(f + g)`) equals the sum of the coe function applied to `f` and `g` separately (`⇑f + ⇑g`). Here, the `coe` notation refers to the coercion of continuous maps to their pointwise function counterparts.
More concisely: For continuous maps $f$ and $g$ from topological space $\alpha$ to a topological space $\beta$ with a continuous addition operation, the pointwise addition of $f$ and $g$ equals their continuous sum: $f + g = \operatorname{coe}(f + g) = \operatorname{coe}(f) + \operatorname{coe}(g)$.
|
ContinuousMap.coe_nsmul
theorem ContinuousMap.coe_nsmul :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
[inst_3 : ContinuousAdd β] (n : ℕ) (f : C(α, β)), ⇑(n • f) = n • ⇑f
This theorem states that for any continuous map `f` from a topological space `α` to an additive monoid `β` (which is also a topological space and supports continuous addition), the action of scalar multiplication `n • f` on `f` corresponds to scalar multiplication `n • ⇑f` applied to the pointwise application of `f`. This is true for all natural numbers `n`. In other words, scalar multiplication of the continuous map can be distributed through to the pointwise application of the map.
More concisely: For any continuous map `f` from a topological space `α` to an additive monoid `β` (and topological space), scalar multiplication `n • f` equals the pointwise application of `n • ⇑f` to `f`, for all natural numbers `n`.
|
ContinuousMap.coe_neg
theorem ContinuousMap.coe_neg :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Neg β]
[inst_3 : ContinuousNeg β] (f : C(α, β)), ⇑(-f) = -⇑f
This theorem states that for any continuous function `f` from a topological space `α` to another topological space `β` that has a negation operation and this negation operation is continuous, the negation of the function `f` is equal to the function that maps each point in `α` to the negation of its image under `f`. In other words, negating the function `f` is the same as applying the function `f` and then negating the result.
More concisely: For any continuous function `f` from a topological space `α` to a topological space `β` with a continuous negation operation, the negation of `f` equals the function that maps each point in `α` to the negation of its image under `f`.
|
ContinuousMap.coe_zero
theorem ContinuousMap.coe_zero :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β],
⇑0 = 0
This theorem states that for any types `α` and `β`, where `α` and `β` have a topological space structure, and `β` also has a zero defined, the continuous function that maps everything to zero (denoted by `⇑0`) is indeed the zero function. In other words, the zero-constant continuous function is the zero element in the space of all continuous functions from `α` to `β`.
More concisely: For any topological spaces `α` and `β` with a zero element in `β`, the continuous function mapping every element of `α` to the zero element of `β` is the zero function in the space of continuous functions from `α` to `β`.
|
ContinuousMap.coe_mul
theorem ContinuousMap.coe_mul :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Mul β]
[inst_3 : ContinuousMul β] (f g : C(α, β)), ⇑(f * g) = ⇑f * ⇑g
This theorem states that for any two continuous maps `f` and `g` from a topological space `α` to a topological space `β` that is also a multiplication space with continuous multiplication, the multiplication of the two continuous maps (`f * g`) is equal to the pointwise multiplication of the functions (`⇑f * ⇑g`). In other words, multiplication of continuous maps in the sense of the algebra of continuous functions corresponds directly to pointwise multiplication of the functions.
More concisely: For any continuous functions `f` and `g` from a topological space to a topological multiplication space, `f * g` equals the pointwise multiplication `⇑f * ⇑g` of their functions.
|
ContinuousMap.compStarAlgHom'_comp
theorem ContinuousMap.compStarAlgHom'_comp :
∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] (𝕜 : Type u_4) [inst_3 : CommSemiring 𝕜] (A : Type u_5)
[inst_4 : TopologicalSpace A] [inst_5 : Semiring A] [inst_6 : TopologicalSemiring A] [inst_7 : Star A]
[inst_8 : ContinuousStar A] [inst_9 : Algebra 𝕜 A] (g : C(Y, Z)) (f : C(X, Y)),
ContinuousMap.compStarAlgHom' 𝕜 A (g.comp f) =
(ContinuousMap.compStarAlgHom' 𝕜 A f).comp (ContinuousMap.compStarAlgHom' 𝕜 A g)
The theorem `ContinuousMap.compStarAlgHom'_comp` states that, for any types `X`, `Y`, `Z`, and `𝕜` along with a type `A` having the structures of topological space, semiring, topological semiring, star operation, continuous star operation and algebra over `𝕜`, the operation `ContinuousMap.compStarAlgHom'` is functorial. In other words, for any continuous maps `f` from `X` to `Y` and `g` from `Y` to `Z`, composing these maps and then applying `ContinuousMap.compStarAlgHom'` is the same as first applying `ContinuousMap.compStarAlgHom'` on each map and then composing the results. This theorem is a formal statement of the compatibility of the `ContinuousMap.compStarAlgHom'` operation with function composition.
More concisely: For any continuous maps `f : X → Y` and `g : Y → Z` between topological semirings `X`, `Y`, `Z` with star operations and algebra structures over a common topological ring, the diagram `ContinuousMap.compStarAlgHom' (f) (ContinuousMap.compStarAlgHom' g) = ContinuousMap.compStarAlgHom' (g ∘ f)` commutes.
|
ContinuousMap.instAddCommGroupContinuousMap.proof_1
theorem ContinuousMap.instAddCommGroupContinuousMap.proof_1 :
∀ {β : Type u_1} [inst : TopologicalSpace β] [inst_1 : AddCommGroup β] [inst_2 : TopologicalAddGroup β],
ContinuousAdd β
This theorem states that for any type `β`, given that `β` is a topological space, an additive commutative group, and a topological additive group, the operation of addition on `β` is continuous. In other words, it says that the sum of two elements in such a group can be calculated in a way that respects the topology's closeness relations.
More concisely: Given a topological space, additive commutative group, and topological additive group `β`, the addition operation on `β` is a continuous function.
|
ContinuousMap.periodic_tsum_comp_add_zsmul
theorem ContinuousMap.periodic_tsum_comp_add_zsmul :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : AddCommGroup X]
[inst_3 : TopologicalAddGroup X] [inst_4 : AddCommMonoid Y] [inst_5 : ContinuousAdd Y] [inst_6 : T2Space Y]
(f : C(X, Y)) (p : X), Function.Periodic (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)))) p
This theorem states that if you have a continuous map `f` from a topological additively commutative group `X` to a topologically continuous additively commutative monoid 'Y', and an element `p` of `X`, then the function obtained by summing up the translates of `f` by the integer multiples of `p` is periodic with period `p`. This is true even if the sum does not converge, in which case it is taken to be the zero function, which is trivially periodic. In other words, the infinite sum over all integers `n` of the composition of `f` with the function that adds `n` times `p` to its input is a periodic function.
More concisely: If `f` is a continuous map from a topological additively commutative group `X` to a topologically continuous additively commutative monoid `Y`, then the function summing up translates of `f` by integer multiples of `p` is periodic with period `p`.
|
Subalgebra.SeparatesPoints.strongly
theorem Subalgebra.SeparatesPoints.strongly :
∀ {α : Type u_1} [inst : TopologicalSpace α] {𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : Field 𝕜]
[inst_3 : TopologicalRing 𝕜] {s : Subalgebra 𝕜 C(α, 𝕜)}, s.SeparatesPoints → (↑s).SeparatesPointsStrongly
The theorem states that in the context of continuous functions into a topological field, if a subalgebra of functions is able to distinguish between points (i.e., for any two different points `x` and `y`, there exists a function `f` in the subalgebra such that `f(x) ≠ f(y)`), then it also strongly separates points. Strong separation of points means that for any two different points and any two distinct field elements `a` and `b`, there exists a function in the subalgebra that maps `x` to `a` and `y` to `b`. This is achieved by applying an affine transformation to the function `f`.
More concisely: If a subalgebra of continuous functions into a topological field distinguishes between points, then it strongly separates points.
|
ContinuousMap.coe_zsmul
theorem ContinuousMap.coe_zsmul :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
[inst_3 : TopologicalAddGroup β] (z : ℤ) (f : C(α, β)), ⇑(z • f) = z • ⇑f
This theorem states that for any two types `α` and `β`, where `α` is a topological space and `β` is both a topological space and an add group, then given a continuous map `f` from `α` to `β` and an integer `z`, the application of the `z`-multiple of the map `f` to any input is equal to `z` times the application of the `f` to that same input. This property holds if `β` also forms a topological add group.
More concisely: Given a continuous map from a topological space to a topological add group, the map's multiplication by an integer preserves the operation, i.e., `(z * f)(x) = z * (f(x))` for all `x` in the topological space.
|
ContinuousMap.coe_one
theorem ContinuousMap.coe_one :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : One β],
⇑1 = 1
This theorem states that for any types `α` and `β`, where `α` is a topological space and `β` is both a topological space and has a defined multiplicative identity (1), the application of the multiplicative identity function (denoted as `⇑1`) is equal to the multiplicative identity itself. In other words, applying the identity function to any element in this context will yield the same element.
More concisely: For any topological spaces `α` and `β` with a multiplicative identity `1` in `β`, the application of the identity function `⇑1` to any element in `β` is equal to the multiplicative identity itself.
|