measurable_mul_unop

Mathlib.MeasureTheory.Group.Arithmetic

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

English

The unop map from αᵐᵒᵖ to α is measurable.

Русский

Отображение unop: αᵐᵒᵖ → α измеримо.

LaTeX

$$$\\text{Measurable}(\\text{unop})$$$

Lean4

@[to_additive]
theorem measurable_mul_unop {α : Type*} [MeasurableSpace α] : Measurable (unop : αᵐᵒᵖ → α) := fun _ => id

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

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

Разделы

Аффилиация

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