Multiplicative action on the completion of a uniform space #
In this file we define typeclasses has_uniform_continuous_const_vadd
and
has_uniform_continuous_const_smul
and prove that a multiplicative action on X
with uniformly
continuous (•) c
can be extended to a multiplicative action on uniform_space.completion X
.
In later files once the additive group structure is set up, we provide
@[class]
structure
has_uniform_continuous_const_vadd
(M : Type v)
(X : Type x)
[_inst_1 _inst_3 : uniform_space X]
[has_vadd M X] :
Prop
- uniform_continuous_const_vadd : ∀ (c : M), uniform_continuous (has_vadd.vadd c)
An additive action such that for all c
, the map λ x, c +ᵥ x
is uniformly continuous.
@[class]
structure
has_uniform_continuous_const_smul
(M : Type v)
(X : Type x)
[_inst_1 _inst_3 : uniform_space X]
[has_scalar M X] :
Prop
- uniform_continuous_const_smul : ∀ (c : M), uniform_continuous (has_scalar.smul c)
A multiplicative action such that for all c
, the map λ x, c • x
is uniformly continuous.
Instances of this typeclass
- has_uniform_continuous_const_smul.op
- uniform_space.completion.normed_space.to_has_uniform_continuous_const_smul
- add_monoid.has_uniform_continuous_const_smul_nat
- add_group.has_uniform_continuous_const_smul_int
- mul_opposite.has_uniform_continuous_const_smul
- uniform_group.to_has_uniform_continuous_const_smul
- uniform_space.completion.has_uniform_continuous_const_smul
@[protected, instance]
def
add_monoid.has_uniform_continuous_const_smul_nat
(X : Type x)
[uniform_space X]
[add_group X]
[uniform_add_group X] :
@[protected, instance]
def
add_group.has_uniform_continuous_const_smul_int
(X : Type x)
[uniform_space X]
[add_group X]
[uniform_add_group X] :
@[protected, instance]
def
has_uniform_continuous_const_vadd.to_has_continuous_const_vadd
(M : Type v)
(X : Type x)
[uniform_space X]
[has_vadd M X]
[has_uniform_continuous_const_vadd M X] :
@[protected, instance]
def
has_uniform_continuous_const_smul.to_has_continuous_const_smul
(M : Type v)
(X : Type x)
[uniform_space X]
[has_scalar M X]
[has_uniform_continuous_const_smul M X] :
theorem
uniform_continuous.const_smul
{M : Type v}
{X : Type x}
{Y : Type y}
[uniform_space X]
[uniform_space Y]
[has_scalar M X]
[has_uniform_continuous_const_smul M X]
{f : Y → X}
(hf : uniform_continuous f)
(c : M) :
uniform_continuous (c • f)
theorem
uniform_continuous.const_vadd
{M : Type v}
{X : Type x}
{Y : Type y}
[uniform_space X]
[uniform_space Y]
[has_vadd M X]
[has_uniform_continuous_const_vadd M X]
{f : Y → X}
(hf : uniform_continuous f)
(c : M) :
uniform_continuous (c +ᵥ f)
@[protected, instance]
def
has_uniform_continuous_const_smul.op
{M : Type v}
{X : Type x}
[uniform_space X]
[has_scalar M X]
[has_scalar Mᵐᵒᵖ X]
[is_central_scalar M X]
[has_uniform_continuous_const_smul M X] :
If a scalar is central, then its right action is uniform continuous when its left action is.
@[protected, instance]
def
mul_opposite.has_uniform_continuous_const_smul
{M : Type v}
{X : Type x}
[uniform_space X]
[has_scalar M X]
[has_uniform_continuous_const_smul M X] :
@[protected, instance]
def
add_opposite.has_uniform_continuous_const_vadd
{M : Type v}
{X : Type x}
[uniform_space X]
[has_vadd M X]
[has_uniform_continuous_const_vadd M X] :
@[protected, instance]
def
uniform_group.to_has_uniform_continuous_const_smul
{G : Type u}
[group G]
[uniform_space G]
[uniform_group G] :
@[protected, instance]
def
uniform_add_group.to_has_uniform_continuous_const_vadd
{G : Type u}
[add_group G]
[uniform_space G]
[uniform_add_group G] :
@[protected, instance]
noncomputable
def
uniform_space.completion.has_vadd
(M : Type v)
(X : Type x)
[uniform_space X]
[has_vadd M X] :
Equations
- uniform_space.completion.has_vadd M X = {vadd := λ (c : M), uniform_space.completion.map (has_vadd.vadd c)}
@[protected, instance]
noncomputable
def
uniform_space.completion.has_scalar
(M : Type v)
(X : Type x)
[uniform_space X]
[has_scalar M X] :
Equations
- uniform_space.completion.has_scalar M X = {smul := λ (c : M), uniform_space.completion.map (has_scalar.smul c)}
@[protected, instance]
def
uniform_space.completion.has_uniform_continuous_const_vadd
(M : Type v)
(X : Type x)
[uniform_space X]
[has_vadd M X] :
@[protected, instance]
def
uniform_space.completion.has_uniform_continuous_const_smul
(M : Type v)
(X : Type x)
[uniform_space X]
[has_scalar M X] :
@[protected, instance]
def
uniform_space.completion.is_central_scalar
(M : Type v)
(X : Type x)
[uniform_space X]
[has_scalar M X]
[has_scalar Mᵐᵒᵖ X]
[is_central_scalar M X] :
@[simp, norm_cast]
theorem
uniform_space.completion.coe_smul
{M : Type v}
{X : Type x}
[uniform_space X]
[has_scalar M X]
[has_uniform_continuous_const_smul M X]
(c : M)
(x : X) :
@[simp, norm_cast]
theorem
uniform_space.completion.coe_vadd
{M : Type v}
{X : Type x}
[uniform_space X]
[has_vadd M X]
[has_uniform_continuous_const_vadd M X]
(c : M)
(x : X) :
@[protected, instance]
noncomputable
def
uniform_space.completion.add_action
(M : Type v)
(X : Type x)
[uniform_space X]
[add_monoid M]
[add_action M X]
[has_uniform_continuous_const_vadd M X] :
Equations
- uniform_space.completion.add_action M X = {to_has_vadd := {vadd := has_vadd.vadd (uniform_space.completion.has_vadd M X)}, zero_vadd := _, add_vadd := _}
@[protected, instance]
noncomputable
def
uniform_space.completion.mul_action
(M : Type v)
(X : Type x)
[uniform_space X]
[monoid M]
[mul_action M X]
[has_uniform_continuous_const_smul M X] :
Equations
- uniform_space.completion.mul_action M X = {to_has_scalar := {smul := has_scalar.smul (uniform_space.completion.has_scalar M X)}, one_smul := _, mul_smul := _}