measurableEmbedding_divRight

Mathlib.MeasureTheory.Group.MeasurableEquiv

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

← MathLib Explorer

English

For any g ∈ G, the map x ↦ x / g is a measurable embedding.

Русский

Для любого g ∈ G отображение x ↦ x / g является измеримым вложением.

LaTeX

$$$\\text{measurableEmbedding\_divRight }(g): \\; x \\mapsto x / g$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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