Structures · Topology

IsBoundedSMul

Mixin typeclass on a scalar action of a metric space α on a metric space β both with distinguished points 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. If [NormedDivisionRing α] [SeminormedAddCommGroup β] [Module α β] are assumed, then prefer writing [NormSMulClass α β] instead of using [IsBoundedSMul α β], since while equivalent, typeclass search can only infer the latter from the former and not vice versa.

Defined in

Mathlib.Topology.MetricSpace.Algebra

Shape

2 explicit arguments · adds dist_smul_pair', dist_pair_smul'