English
If a group G acts on α by measurable maps, then each element c ∈ G defines a measurable automorphism of α.
Русский
Если группа G действует на пространстве α отображениями, измеримыми по отношению к α, то каждый элемент c ∈ G задаёт измеримое автоморфизм α.
LaTeX
$$$$ \\forall c \\in G,\\; \\exists \\varphi_c: \\alpha \\to \\alpha \\text{ measurable bijection with } \\varphi_c(x) = c \\cdot x. $$$$
Lean4
/-- If a group `G` acts on `α` by measurable maps, then each element `c : G` defines a measurable
automorphism of `α`. -/
@[to_additive (attr := simps! -fullyApplied toEquiv apply) /--
If an additive group `G` acts on `α` by measurable maps, then each element `c : G`
defines a measurable automorphism of `α`. -/
]
def smul (c : G) : α ≃ᵐ α where
toEquiv := MulAction.toPerm c
measurable_toFun := measurable_const_smul c
measurable_invFun := measurable_const_smul c⁻¹
