measurable_leOnePart

Mathlib.MeasureTheory.Order.Group.Lattice

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

← MathLib Explorer

English

The map leOnePart: α → α is measurable (under MeasurableSup).

Русский

Функция leOnePart: α → α измерима (при условии MeasurableSup).

LaTeX

$$$\operatorname{Measurable}(\mathrm{leOnePart})$$$

Lean4

@[to_additive (attr := measurability)]
theorem measurable_leOnePart [MeasurableSup α] : Measurable (leOnePart : α → α) :=
  (measurable_sup_const _).comp measurable_inv

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

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

Разделы

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

Аффилиация

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