aeSeq_eq_mk_of_mem_aeSeqSet

Mathlib.MeasureTheory.Function.AEMeasurableSequence

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

← MathLib Explorer

English

If x is in the AESeqSet, then aeSeq hf p i x equals (hf i).mk (f i) x for every i.

Русский

Если x принадлежит AESeqSet, то aeSeq hf p i x равно (hf i).mk (f i) x для каждого i.

LaTeX

$$$$ \ aeSeq hf p i x = (hf i).mk (f i) x $$$$

Lean4

theorem aeSeq_eq_mk_of_mem_aeSeqSet (hf : ∀ i, AEMeasurable (f i) μ) {x : α} (hx : x ∈ aeSeqSet hf p) (i : ι) :
    aeSeq hf p i x = (hf i).mk (f i) x := by simp only [aeSeq, hx, if_true]

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

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

Разделы

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

Аффилиация

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