aestronglyMeasurable

Mathlib.MeasureTheory.Function.UniformIntegrable

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

← MathLib Explorer

English

If f is Uniformly Integrable, then each component f_i is AEStronglyMeasurable.

Русский

Если f является UniformIntegrable, то каждый компонент f_i является AEStronglyMeasurable.

LaTeX

$$$\\forall i,\\\\ AEStronglyMeasurable (f i) μ$$$

Lean4

protected theorem aestronglyMeasurable {f : ι → α → β} {p : ℝ≥0∞} (hf : UniformIntegrable f p μ) (i : ι) :
    AEStronglyMeasurable (f i) μ :=
  hf.1 i

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

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

Разделы

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

Аффилиация

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