measurableEmbedding_divLeft

Mathlib.MeasureTheory.Group.MeasurableEquiv

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

← MathLib Explorer

English

The underlying Equiv of mulLeft₀ g hg is Equiv.mulLeft₀ g hg.

Русский

Умолчательная эквивалентность mulLeft₀ g hg равна Equiv.mulLeft₀ g hg.

LaTeX

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

Lean4

@[to_additive]
theorem _root_.measurableEmbedding_divLeft [MeasurableMul G] [MeasurableInv G] (g : G) :
    MeasurableEmbedding fun x ↦ g / x :=
  (divLeft g).measurableEmbedding

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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