English
If a measure μ on a space α is invariant under the action of a group G, then μ is invariant under the restricted action of any subgroup H ≤ G (i.e., the subgroup inherits the invariance property from G).
Русский
Если мера μ на пространстве α инвариантна относительно группы G, то она инвариантна также относительно любой подгруппы H ≤ G (то есть подгруппа наследует инвариантность от G).
LaTeX
$$$\forall H \le G, \ \forall h \in H,\ map(h\cdot)\mu = \mu \quad\text{equivalently}\quad \forall A\in\mathcal{B}(\alpha),\ μ((h\cdot)^{-1}A)=μ(A).$$$
Lean4
@[to_additive]
instance smulInvariantMeasure {G α : Type*} [Group G] [MulAction G α] [MeasurableSpace α] {μ : Measure α}
[SMulInvariantMeasure G α μ] (H : Subgroup G) : SMulInvariantMeasure H α μ :=
⟨fun y s hs => by convert SMulInvariantMeasure.measure_preimage_smul (μ := μ) (y : G) hs⟩
