stronglyMeasurable

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.simpleFunc.stronglyMeasurable

English

The function toSimpleFunc f is strongly measurable.

Русский

Функция toSimpleFunc f сильно измерима.

LaTeX

$$$\mathrm{StronglyMeasurable}(\mathrm{toSimpleFunc}(f))$$$

Lean4

protected theorem stronglyMeasurable (f : Lp.simpleFunc E p μ) : StronglyMeasurable (toSimpleFunc f) :=
  (toSimpleFunc f).stronglyMeasurable

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

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

Разделы

Аффилиация

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