Theorems · Inductive type · general topology

IsBoundedSMul

(α : Type u_1) →
  (β : Type u_2) → [PseudoMetricSpace α] → [PseudoMetricSpace β] → [Zero α] → [Zero β] → [SMul α β] → Prop

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

Cited by

329 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 4 definitions · uses no axioms

Assumes

PseudoMetricSpacePseudoMetricSpaceZeroZeroSMul