measurableEmbedding_mulRight₀

Mathlib.MeasureTheory.Group.MeasurableEquiv

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

English

The equivalence mulRight₀ g hg has underlying Equiv.mulRight₀ g hg.

Русский

Эквивалентность mulRight₀ g hg имеет надмножество Equiv.mulRight₀ g hg.

LaTeX

$$$(\\mathrm{mulRight}_{0}(g, hg)).toEquiv = \\mathrm{Equiv.mulRight}_{0}(g, hg)$$$

Lean4

theorem _root_.measurableEmbedding_mulRight₀ {g : G₀} (hg : g ≠ 0) : MeasurableEmbedding fun x => x * g :=
  (mulRight₀ g hg).measurableEmbedding

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

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

Разделы

Аффилиация

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