Compatibility of algebraic operations with metric space structures #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define mixin typeclasses
has_bounded_smul expressing compatibility of multiplication, addition and scalar-multiplication
operations with an underlying metric space structure. The intended use case is to abstract certain
properties shared by normed groups and by
Implementation notes #
We deduce a
has_continuous_mul instance from
has_lipschitz_mul, etc. In principle there should
be an intermediate typeclass for uniform spaces, but the algebraic hierarchy there (see
uniform_group) is structured differently.
has_lipschitz_add M says that the addition
(+) : X × X → X is Lipschitz jointly in
the two arguments.
has_lipschitz_mul M says that the multiplication
(*) : X × X → X is Lipschitz jointly
in the two arguments.
The Lipschitz constant of an
The Lipschitz constant of a monoid
- dist_smul_pair' : ∀ (x : α) (y₁ y₂ : β), has_dist.dist (x • y₁) (x • y₂) ≤ has_dist.dist x 0 * has_dist.dist y₁ y₂
- dist_pair_smul' : ∀ (x₁ x₂ : α) (y : β), has_dist.dist (x₁ • y) (x₂ • y) ≤ has_dist.dist x₁ x₂ * has_dist.dist y 0
Mixin typeclass on a scalar action of a metric space
α on a metric space
β both with
0, requiring compatibility of the action in the sense that
dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂ and
dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0.
has_bounded_smul on a metric-space scalar action implies continuity of the
If a scalar is central, then its right action is bounded when its left action is.