# mathlibdocumentation

topology.algebra.uniform_mul_action

# 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

• uniform_space.completion.distrib_mul_action
• uniform_space.completion.mul_action_with_zero
• uniform_space.completion.module
@[class]
structure has_uniform_continuous_const_vadd (M : Type v) (X : Type x) [_inst_1 _inst_3 : uniform_space X] [ X] :
Prop
• uniform_continuous_const_vadd : ∀ (c : M),

An additive action such that for all c, the map λ x, c +ᵥ x is uniformly continuous.

Instances of this typeclass
@[class]
structure has_uniform_continuous_const_smul (M : Type v) (X : Type x) [_inst_1 _inst_3 : uniform_space X] [ X] :
Prop
• uniform_continuous_const_smul : ∀ (c : M),

A multiplicative action such that for all c, the map λ x, c • x is uniformly continuous.

Instances of this typeclass
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem uniform_continuous.const_smul {M : Type v} {X : Type x} {Y : Type y} [ X] {f : Y → X} (hf : uniform_continuous f) (c : M) :
theorem uniform_continuous.const_vadd {M : Type v} {X : Type x} {Y : Type y} [ X] {f : Y → X} (hf : uniform_continuous f) (c : M) :
@[protected, instance]
def has_uniform_continuous_const_smul.op {M : Type v} {X : Type x} [ X] [ X] [ 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} [ X]  :
@[protected, instance]
def add_opposite.has_uniform_continuous_const_vadd {M : Type v} {X : Type x} [ X]  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def uniform_space.completion.has_vadd (M : Type v) (X : Type x) [ X] :
Equations
@[protected, instance]
noncomputable def uniform_space.completion.has_scalar (M : Type v) (X : Type x) [ X] :
Equations
@[protected, instance]
def uniform_space.completion.has_uniform_continuous_const_vadd (M : Type v) (X : Type x) [ X] :
@[protected, instance]
def uniform_space.completion.has_uniform_continuous_const_smul (M : Type v) (X : Type x) [ X] :
@[protected, instance]
def uniform_space.completion.is_central_scalar (M : Type v) (X : Type x) [ X] [ X] [ X] :
@[simp, norm_cast]
theorem uniform_space.completion.coe_smul {M : Type v} {X : Type x} [ X] (c : M) (x : X) :
(c x) = c x
@[simp, norm_cast]
theorem uniform_space.completion.coe_vadd {M : Type v} {X : Type x} [ X] (c : M) (x : X) :
(c +ᵥ x) = c +ᵥ x
@[protected, instance]
noncomputable def uniform_space.completion.add_action (M : Type v) (X : Type x) [add_monoid M] [ X]  :
Equations
@[protected, instance]
noncomputable def uniform_space.completion.mul_action (M : Type v) (X : Type x) [monoid M] [ X]  :
Equations