UniformSpace.Completion.coe_smul
theorem UniformSpace.Completion.coe_smul :
∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : SMul M X] [inst_2 : UniformContinuousConstSMul M X]
(c : M) (x : X), ↑X (c • x) = c • ↑X x
This theorem states that in a uniform space `X` that supports scalar multiplication by elements from a type `M`, if the scalar multiplication is uniformly continuous, then the scalar multiplication commutes with the uniform space completion embedding. Specifically, for any scalar `c` from `M` and any element `x` from `X`, the completion of the result of scalar multiplying `x` by `c` is equal to the result of scalar multiplying the completion of `x` by `c`.
More concisely: In a uniform space with scalar multiplication by type `M`, if scalar multiplication is uniformly continuous, then the completion of the product of an element and a scalar is equal to the product of their completions.
|
uniformContinuousConstSMul_of_continuousConstSMul
theorem uniformContinuousConstSMul_of_continuousConstSMul :
∀ (R : Type u) (M : Type v) [inst : Monoid R] [inst_1 : AddCommGroup M] [inst_2 : DistribMulAction R M]
[inst_3 : UniformSpace M] [inst_4 : UniformAddGroup M] [inst_5 : ContinuousConstSMul R M],
UniformContinuousConstSMul R M
This theorem states that for any types `R` and `M`, where `R` is a monoid, `M` is an additive commutative group, `M` is a uniform space and a uniform additive group, and `R` has a distributive multiplication action on `M` that is continuous, then the constant scalar multiplication of `R` on `M` is uniformly continuous. However, this cannot be an instance because it would form a loop with the theorem `UniformContinuousConstSMul.to_continuousConstSMul`.
More concisely: If `R` is a continuous, distributive monoid action on an additive commutative group `M`, which is also a uniform space and a uniform additive group, then constant scalar multiplication by elements of `R` on `M` is uniformly continuous.
|