instMeasurableSMul — Mathlib

English

Restriction of SMul to a Subgroup inherits a measurable SMul structure on α; i.e., the action of the subgroup is measurable.

Русский

Действие подгруппы на α поSmul наследует измеримость: действие подгруппы измеримо.

LaTeX

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

Lean4

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

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