setToFun_undef

Mathlib.MeasureTheory.Integral.SetToL1

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

English

If f is not integrable, then setToFun μ T hT f = 0.

Русский

Если f не интегрируем, то setToFun μ T hT f = 0.

LaTeX

$$$\text{If } \neg \text{Integrable}(f, μ) \Rightarrow setToFun\, μ\, T\, h_T\, f = 0$$$

Lean4

theorem setToFun_undef (hT : DominatedFinMeasAdditive μ T C) (hf : ¬Integrable f μ) : setToFun μ T hT f = 0 :=
  dif_neg hf

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

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

Разделы

Аффилиация

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