mathlib3 documentation

topology.algebra.uniform_mul_action

Multiplicative action on the completion of a uniform space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

TODO: Generalise the results here from the concrete completion to any abstract_completion.

@[class]
structure has_uniform_continuous_const_vadd (M : Type v) (X : Type x) [uniform_space X] [has_vadd M X] :
Prop

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

Instances of this typeclass

A distrib_mul_action that is continuous on a uniform group is uniformly continuous. This can't be an instance due to it forming a loop with has_uniform_continuous_const_smul.to_has_continuous_const_smul

@[protected, instance]

The action of semiring.to_module is uniformly continuous.

@[protected, instance]

If a scalar action is central, then its right action is uniform continuous when its left action is.

@[protected, instance]

If an additive action is central, then its right action is uniform continuous when its left action,is.

@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem uniform_space.completion.coe_smul {M : Type v} {X : Type x} [uniform_space X] [has_smul M X] [has_uniform_continuous_const_smul M X] (c : M) (x : X) :
(c x) = c 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) :
(c +ᵥ x) = c +ᵥ x