ContinuousAffineMap.coe_injective
theorem ContinuousAffineMap.coe_injective :
∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R]
[inst_1 : AddCommGroup V] [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P]
[inst_5 : AddCommGroup W] [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q],
Function.Injective DFunLike.coe
The theorem `ContinuousAffineMap.coe_injective` states that for any ring `R`, additive commutative groups `V` and `W`, modules `V` and `W` over `R`, topological spaces `P` and `Q`, and additive torsors `V` over `P` and `W` over `Q`, the function `DFunLike.coe`, which is a coercion function from `F` to a function, is injective. In other words, if for two continuous affine maps, the corresponding functions (obtained by applying `DFunLike.coe`) are equal, then the original continuous affine maps are also equal.
More concisely: For any continuous affine maps between additive commutative groups made into topological spaces as modules over a ring, the coercion function from the space of functions to the space of continuous affine maps is injective.
|
ContinuousAffineMap.coe_smul
theorem ContinuousAffineMap.coe_smul :
∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
[inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
[inst_6 : Module R W] {S : Type u_8} [inst_7 : TopologicalSpace W] [inst_8 : Monoid S]
[inst_9 : DistribMulAction S W] [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] (t : S)
(f : P →A[R] W), ⇑(t • f) = t • ⇑f
The theorem `ContinuousAffineMap.coe_smul` states that for any ring `R`, additive commutative groups `V` and `W`, a module `V` over `R`, a topological space `P` with `V` as its torsor, a monoid `S`, and a continuous multiplication operation `S` on `W` that commutes with `R`, when you scale a continuous affine map `f` from `P` to `W` by a scalar `t` from `S`, applying this scaled map is the same as scaling the result of applying `f`. In equation form, it can be represented as `⇑(t • f) = t • ⇑f`. This theorem is about the interaction of continuous affine maps with scalar multiplication.
More concisely: For any continuous affine map from a torsor to a module over a ring, and any scalar in the monoid with commuting continuous multiplication on the module, the application of the scaled map is equal to scaling the result of applying the map.
|
ContinuousAffineMap.ext
theorem ContinuousAffineMap.ext :
∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R]
[inst_1 : AddCommGroup V] [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P]
[inst_5 : AddCommGroup W] [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q]
{f g : P →A[R] Q}, (∀ (x : P), f x = g x) → f = g
This theorem states that for any two continuous affine maps 'f' and 'g' from a vector space 'P' to another vector space 'Q', if for every point 'x' in 'P', the image of 'x' under 'f' and 'g' are the same, then 'f' and 'g' are the same continuous affine map. Here, the vector spaces 'P' and 'Q' are over a ring 'R', and have underlying additive abelian groups 'V' and 'W', respectively. The vector spaces are also topological spaces, and 'P' and 'Q' are torsor spaces over 'V' and 'W', respectively.
More concisely: Given continuous affine maps $f, g : P \to Q$ between topological vector spaces $P$ and $Q$ over a ring $R$, if $f(x) = g(x)$ for all $x \in P$, then $f = g$.
|
ContinuousAffineMap.continuous
theorem ContinuousAffineMap.continuous :
∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R]
[inst_1 : AddCommGroup V] [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P]
[inst_5 : AddCommGroup W] [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q]
(f : P →A[R] Q), Continuous ⇑f
This theorem asserts that for any continuous affine map `f` from a topological vector space `P` to another topological vector space `Q`, the function `f` is continuous. Here, `P` and `Q` are add-torsors over the modules `V` and `W` respectively, both of which are modules over a ring `R`. The continuity of `f` holds under the assumptions that `V` and `W` are additive commutative groups and `R` is a ring.
More concisely: Given topological vector spaces P and Q over rings R, and a continuous affine map f from P to Q where P and Q are additive commutative groups, then f is a continuous function.
|