Theorems · Definition · general topology

IsometryEquiv.constSMul

{G : Type v} →
  {X : Type w} →
    [inst : PseudoEMetricSpace X] → [inst_1 : Group G] → [inst_2 : MulAction G X] → [IsIsometricSMul G X] → G → X ≃ᵢ X

If a group G acts on X by isometries, then IsometryEquiv.constSMul is the isometry of X given by multiplication of a constant element of the group.

Defined in

Mathlib.Topology.MetricSpace.IsometricSMul

Cited by

8 results in Mathlib

Foundations

Depth 150 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpaceGroupMulActionIsIsometricSMul