leOnePart

Mathlib.MeasureTheory.Order.Group.Lattice

URI: https://scilib.ai/kg/mathlib#Measurable.leOnePart

← MathLib Explorer

English

If f is measurable, then x ↦ leOnePart(f(x)) is measurable.

Русский

Если f измерима, то x ↦ leOnePart(f(x)) измерима.

LaTeX

$$$\operatorname{Measurable}(f) \Rightarrow \operatorname{Measurable}\bigl(x \mapsto \mathrm{leOnePart}(f(x))\bigr)$$$

Lean4

@[to_additive (attr := measurability)]
protected theorem leOnePart [MeasurableSup α] (hf : Measurable f) : Measurable fun x ↦ leOnePart (f x) :=
  measurable_leOnePart.comp hf

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

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

Разделы

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

Аффилиация

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