ContinuousAddMonoidHomClass.map_continuous
theorem ContinuousAddMonoidHomClass.map_continuous :
∀ {F : Type u_1} {A : outParam (Type u_7)} {B : outParam (Type u_8)} [inst : AddMonoid A] [inst_1 : AddMonoid B]
[inst_2 : TopologicalSpace A] [inst_3 : TopologicalSpace B] [inst_4 : FunLike F A B]
[self : ContinuousAddMonoidHomClass F A B] (f : F), Continuous ⇑f
This theorem states that for any type `F` and types `A` and `B` with additional structures: `A` and `B` are additive monoids and are equipped with a topology, and `F` has a function-like structure from `A` to `B` - then, if `F` has the structure of a continuous additive monoid homomorphism, any element `f` of type `F` is a continuous function when coerced to a function from `A` to `B`. In short, the theorem asserts the continuity of the map in the context of a continuous additive monoid homomorphism.
More concisely: Given a continuous additive monoid homomorphism between additive monoids equipped with topologies, the homomorphism is a continuous function between the underlying topological spaces.
|
ContinuousMonoidHom.continuous_toFun
theorem ContinuousMonoidHom.continuous_toFun :
∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
[inst_3 : TopologicalSpace B] (self : ContinuousMonoidHom A B), Continuous self.toFun
This theorem states that for any two types `A` and `B` which are equipped with a monoid structure and a topological space structure, if there exists a continuous monoid homomorphism from `A` to `B`, then the function underlying this homomorphism (accessed via `.toFun`) is continuous in the topological sense.
More concisely: If `f` is a continuous monoid homomorphism between topological monoids `(A, ⊕_A, τ_A)` and `(B, ⊕_B, τ_B)`, then `f.toFun` is a continuous function between the topological spaces `(A, τ_A)` and `(B, τ_B)`.
|
ContinuousAddMonoidHom.continuous_toFun
theorem ContinuousAddMonoidHom.continuous_toFun :
∀ {A : Type u_7} {B : Type u_8} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
[inst_3 : TopologicalSpace B] (self : ContinuousAddMonoidHom A B), Continuous self.toFun
This theorem states that for any two types `A` and `B` which are both additive monoids and topological spaces, the function (`toFun`) of a continuous additive monoid homomorphism from `A` to `B` is itself continuous. A continuous additive monoid homomorphism is a function that preserves the addition operation and is continuous with respect to the topologies on `A` and `B`.
More concisely: If `f` is a continuous function between two additive monoids and topological spaces `A` and `B` that preserves addition, then `f` is a continuous homomorphism.
|
ContinuousAddMonoidHom.ext
theorem ContinuousAddMonoidHom.ext :
∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
[inst_3 : TopologicalSpace B] {f g : ContinuousAddMonoidHom A B}, (∀ (x : A), f x = g x) → f = g
This theorem states that for any two continuous additive monoid homomorphisms `f` and `g` from one add monoid `A` to another add monoid `B`, where both `A` and `B` are topological spaces, if `f` and `g` map any element `x` from `A` to the same element in `B` (i.e., `f(x) = g(x)` for all `x` in `A`), then `f` and `g` are the same continuous additive monoid homomorphisms. In other words, two continuous additive monoid homomorphisms are the same if they agree on all elements of the domain.
More concisely: If two continuous additive monoid homomorphisms between topological add monoids agree on all elements, they are equal.
|
ContinuousMonoidHomClass.map_continuous
theorem ContinuousMonoidHomClass.map_continuous :
∀ {F : Type u_1} {A : outParam (Type u_7)} {B : outParam (Type u_8)} [inst : Monoid A] [inst_1 : Monoid B]
[inst_2 : TopologicalSpace A] [inst_3 : TopologicalSpace B] [inst_4 : FunLike F A B]
[self : ContinuousMonoidHomClass F A B] (f : F), Continuous ⇑f
The theorem `ContinuousMonoidHomClass.map_continuous` states that for any type `F`, and two other types `A` and `B` (with `A` and `B` being monoids and also having a topological space structure), if `F` has a function-like relationship with `A` and `B`, and there is a continuous monoid homomorphism from `A` to `B` defined in terms of `F`, then the function represented by any term of type `F` is continuous. In other words, this theorem is about the continuity of a function under the condition of being a monoid homomorphism in a topological space.
More concisely: If `F` is a function-like type, `A` and `B` are monoid topological spaces, and `f : A →ᵢ B` is a continuous monoid homomorphism represented by a term of type `F A →ᵢ B`, then `F` is a continuous function.
|
ContinuousMonoidHom.ext
theorem ContinuousMonoidHom.ext :
∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
[inst_3 : TopologicalSpace B] {f g : ContinuousMonoidHom A B}, (∀ (x : A), f x = g x) → f = g
This theorem states that for any two continuous monoid homomorphisms `f` and `g` from a topological monoid `A` to another topological monoid `B`, if for all elements `x` in `A`, the images under `f` and `g` are the same, i.e., `f x = g x`, then `f` and `g` are the same continuous monoid homomorphism. In more mathematical terms, it asserts the uniqueness of continuous monoid homomorphisms between topological monoids.
More concisely: Given topological monoids A and B, and continuous monoid homomorphisms f and g from A to B with the property that f(x) = g(x) for all x in A, then f = g.
|
ContinuousAddMonoidHom.inducing_toContinuousMap
theorem ContinuousAddMonoidHom.inducing_toContinuousMap :
∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
[inst_3 : TopologicalSpace B], Inducing ContinuousAddMonoidHom.toContinuousMap
The theorem `ContinuousAddMonoidHom.inducing_toContinuousMap` states that for any types `A` and `B`, given instances of `A` and `B` as additive monoids and also as topological spaces, the function `ContinuousAddMonoidHom.toContinuousMap` that reinterprets a `ContinuousAddMonoidHom` as a `ContinuousMap`, is an inducing function. In other words, the topology on `B` is the coarsest that makes this function continuous, meaning that the function's continuity is preserved under the mapping from `A` to `B`.
More concisely: Given types `A` and `B` with instances of additive monoid and topological spaces structures, the function `ContinuousAddMonoidHom.toContinuousMap` from `ContinuousAddMonoidHom` to `ContinuousMap` is the greatest continuous function between the structures, preserving the additive monoid homomorphism property.
|
ContinuousMonoidHom.inducing_toContinuousMap
theorem ContinuousMonoidHom.inducing_toContinuousMap :
∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
[inst_3 : TopologicalSpace B], Inducing ContinuousMonoidHom.toContinuousMap
This theorem states that for any two types `A` and `B`, given that `A` and `B` are both monoids and topological spaces, the function `ContinuousMonoidHom.toContinuousMap`, which transforms a continuous monoid homomorphism between `A` and `B` into a continuous map, is an inducing function. In the context of topology, an inducing function creates a topology on the domain that makes the function continuous.
More concisely: Given two monoid and topological spaces `A` and `B` and a continuous monoid homomorphism `f : A → B`, the function `ContinuousMonoidHom.toContinuousMap f` is a continuous function.
|