pos_part

Mathlib.MeasureTheory.Function.L1Space.Integrable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Integrable.pos_part

English

If f is integrable, then the positive part max(f,0) is integrable as well.

Русский

Если f интегрируема, то положительная часть max(f,0) интегрируема.

LaTeX

$$Integrable f μ → Integrable (fun a => max (f a) 0) μ$$

Lean4

@[fun_prop]
theorem pos_part {f : α → ℝ} (hf : Integrable f μ) : Integrable (fun a => max (f a) 0) μ := by constructor <;> fun_prop

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

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

Разделы

Аффилиация

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