measurableEmbedding_mulRight

Mathlib.MeasureTheory.Group.MeasurableEquiv

URI: https://scilib.ai/kg/mathlib#measurableEmbedding_mulRight

English

For each g, the map x ↦ x g is a measurable embedding.

Русский

Для каждого g отображение x ↦ x g является измеримым вложением.

LaTeX

$$$$ \\text{MeasurableEmbedding}(\\,\\,x \\mapsto x g\\,): G \\to G. $$$$

Lean4

@[to_additive]
theorem _root_.measurableEmbedding_mulRight (g : G) : MeasurableEmbedding fun x => x * g :=
  (mulRight g).measurableEmbedding

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

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

Разделы

Аффилиация

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