measurable_oneLePart — Mathlib

English

Let α be a lattice with a measurable supremum operation. Then the map x ↦ oneLePart(x) is measurable.

Русский

Пусть α — решётка с измеримой операцией взятия supremum; отображение x ↦ oneLePart(x) измеримо.

LaTeX

$$$\operatorname{Measurable}(\mathrm{oneLePart} : \alpha \to \alpha)$$$

Lean4

@[to_additive (attr := measurability)]
theorem measurable_oneLePart [MeasurableSup α] : Measurable (oneLePart : α → α) :=
  measurable_sup_const _

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