instSMulInvariantMeasureSubtypeMemSubmonoidOfIsMulLeftInvariant

English

For a monoid G and a submonoid s ⊆ G, if μ is left-invariant under G, then the restricted measure on the subtype {x ∈ G | x ∈ s} remains SMulInvariantMeasure for the action of G on that subtype.

Русский

Для моноида G и подмоноида s ⊆ G, если μ слева инвариантна относительно G, то ограниченная мера на подтипе {x ∈ G | x ∈ s} сохраняет SMulInvariantMeasure для действия G над этим подтипом.

LaTeX

$$$\\text{SMulInvariantMeasure}\\{x\\in G\\mid x\\in s\\} \\, \\mu$$$

Lean4

@[to_additive]
instance [Monoid G] (s : Submonoid G) [IsMulLeftInvariant μ] : SMulInvariantMeasure { x // x ∈ s } G μ :=
  ⟨fun ⟨x, _⟩ _ h ↦ IsMulLeftInvariant.smulInvariantMeasure.1 x h⟩

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