setToFun_eq_setToL1

Mathlib.MeasureTheory.Integral.SetToL1

URI: https://scilib.ai/kg/mathlib#MeasureTheory.L1.setToFun_eq_setToL1

← MathLib Explorer

English

For f integrable, setToFun μ T hT f equals L1.setToL1 hT f.

Русский

Для интегрируемой f имеем setToFun μ T hT f = L1.setToL1 hT f.

LaTeX

$$$setToFun\, \mu\, T\, h_T\, f = L1.setToL1\, h_T\, f$$$

Lean4

theorem setToFun_eq_setToL1 (hT : DominatedFinMeasAdditive μ T C) (f : α →₁[μ] E) :
    setToFun μ T hT f = L1.setToL1 hT f := by rw [setToFun_eq hT (L1.integrable_coeFn f), Integrable.toL1_coeFn]

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

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

Разделы

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

Аффилиация

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