aeSeqSet_measurableSet

Mathlib.MeasureTheory.Function.AEMeasurableSequence

URI: https://scilib.ai/kg/mathlib#aeSeq.aeSeqSet_measurableSet

English

The set aeSeqSet hf p is measurable whenever each f i is AEMeasurable.

Русский

Множество aeSeqSet hf p измеримо, когда каждый f i является AEMeasurable.

LaTeX

$$$ \MeasurableSet( aeSeqSet\, hf\, p ) $$$

Lean4

theorem aeSeqSet_measurableSet {hf : ∀ i, AEMeasurable (f i) μ} : MeasurableSet (aeSeqSet hf p) :=
  (measurableSet_toMeasurable _ _).compl

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

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

Разделы

Аффилиация

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