measurable — Mathlib

English

For any Lp.simpleFunc f, the associated simple function toSimpleFunc f is measurable.

Русский

Для любой простой функции Lp.simpleFunc сопоставленная функция toSimpleFunc f измерима.

LaTeX

$$$\text{Measurable}(\mathrm{toSimpleFunc}(f))$$$

Lean4

/-- `(toSimpleFunc f)` is measurable. -/
@[measurability]
protected theorem measurable [MeasurableSpace E] (f : Lp.simpleFunc E p μ) : Measurable (toSimpleFunc f) :=
  (toSimpleFunc f).measurable

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