isClosed_aestronglyMeasurable

Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.isClosed_aestronglyMeasurable

← MathLib Explorer

English

The set {f ∈ Lp F p μ | AEStronglyMeasurable[m] f μ} is closed.

Русский

Множество {f ∈ Lp ... | AEStronglyMeasurable[m] f μ} замкнуто.

LaTeX

$$$\text{IsClosed}\{f:\ Lp F p μ \mid AEStronglyMeasurable[m] f μ\}$$$

Lean4

theorem isClosed_aestronglyMeasurable [Fact (1 ≤ p)] [CompleteSpace F] (hm : m ≤ m0) :
    IsClosed {f : Lp F p μ | AEStronglyMeasurable[m] f μ} :=
  IsComplete.isClosed (isComplete_aestronglyMeasurable hm)

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

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

Разделы

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

Аффилиация

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