Isometric actions of submonoids and subgroups

A submonoid or subgroup of a monoid acting by isometries acts by isometries through the restricted action. Mathlib registers the restricted action itself, but not this property of it; these instances let theorems about isometric actions apply directly to a subgroup, for example to a discrete subgroup of PSL(2, ℝ) acting on the upper half-plane.

instance Submonoid.isIsometricSMul {M : Type u_1} {X : Type u_2} [PseudoEMetricSpace X] [MulOneClass M] [SMul M X] [IsIsometricSMul M X] (S : Submonoid M) : IsIsometricSMul (↥S) X

A submonoid of a monoid acting by isometries acts by isometries.

instance AddSubmonoid.isIsometricVAdd {M : Type u_1} {X : Type u_2} [PseudoEMetricSpace X] [AddZeroClass M] [VAdd M X] [IsIsometricVAdd M X] (S : AddSubmonoid M) : IsIsometricVAdd (↥S) X

An additive submonoid of an additive monoid acting by isometries acts by isometries.

instance Subgroup.isIsometricSMul {M : Type u_1} {X : Type u_2} [PseudoEMetricSpace X] [Group M] [SMul M X] [IsIsometricSMul M X] (S : Subgroup M) : IsIsometricSMul (↥S) X

A subgroup of a group acting by isometries acts by isometries.

instance AddSubgroup.isIsometricVAdd {M : Type u_1} {X : Type u_2} [PseudoEMetricSpace X] [AddGroup M] [VAdd M X] [IsIsometricVAdd M X] (S : AddSubgroup M) : IsIsometricVAdd (↥S) X

An additive subgroup of an additive group acting by isometries acts by isometries.