instMeasurableConstSMul — Mathlib

English

Restriction of a measurable constant-smul action to a Subgroup G yields a measurable-constant-smul action on the subtype of G.

Русский

Ограничение измеримого константного действия на подгруппу G даёт измеримое константное действие на подтипе G.

LaTeX

$$$\text{MeasurableConstSMul}(\text{Subtype } x:\, x\in G, \alpha)$$$

Lean4

@[to_additive]
instance instMeasurableConstSMul {G α} [MeasurableSpace α] [Group G] [MulAction G α] [MeasurableConstSMul G α]
    (s : Subgroup G) : MeasurableConstSMul s α :=
  s.toSubmonoid.instMeasurableConstSMul

Похожие утверждения