mem_aestabilizer

Mathlib.MeasureTheory.Group.AEStabilizer

URI: https://scilib.ai/kg/mathlib#MulAction.mem_aestabilizer

English

Membership in aestabilizer is equivalent to the almost-everywhere equality of the translated sets.

Русский

Членство в aestabilizer эквивалентно почти в равенству переходящих множеств.

LaTeX

$$$g \in \mathrm{aestabilizer}(G,\mu,s) \iff g\cdot s =^{\mu} s$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_aestabilizer : g ∈ aestabilizer G μ s ↔ g • s =ᵐ[μ] s :=
  .rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru