setToFun_eq

Mathlib.MeasureTheory.Integral.SetToL1

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

English

If f is integrable, then 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 (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ) :
    setToFun μ T hT f = L1.setToL1 hT (hf.toL1 f) :=
  dif_pos hf

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

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

Разделы

Аффилиация

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