aestronglyMeasurable

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

← MathLib Explorer

English

The AEStronglyMeasurable property for toSimpleFunc f holds via a derivation from measurability.

Русский

Свойство AEStronglyMeasurable для toSimpleFunc f следует из измеримости.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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