integral_nonneg

Mathlib.MeasureTheory.Integral.Bochner.Basic

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

English

Let f, g be integrable and f ≤ᵐ g a.e. Then the integrals satisfy ∫ f ≤ ∫ g.

Русский

Пусть f, g интегрируемы и f ≤ᵐ g почти везде; тогда ∫ f ≤ ∫ g.

LaTeX

$$$f,g:\\alpha\\to E$, hf, hg integrable, h: f \\le^a_e g \\Rightarrow \\int f \\le \\int g$.$$

Lean4

theorem integral_nonneg {f : α → E} (hf : 0 ≤ f) : 0 ≤ ∫ x, f x ∂μ :=
  integral_nonneg_of_ae (ae_of_all _ hf)

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

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

Разделы

Аффилиация

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