lintegral_sub_le

Mathlib.MeasureTheory.Integral.Lebesgue.Sub

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

← MathLib Explorer

English

If f is measurable, then ∫ g − ∫ f ≤ ∫ g − f.

Русский

Если f измерима, то ∫ g − ∫ f ≤ ∫ g − f.

LaTeX

$$$(hf : Measurable f) \\Rightarrow ∫⁻ x, g(x) ∂μ - ∫⁻ x, f(x) ∂μ ≤ ∫⁻ x, g(x) ∂μ - ∫⁻ x, f(x) ∂μ$$$

Lean4

theorem lintegral_sub_le (f g : α → ℝ≥0∞) (hf : Measurable f) : ∫⁻ x, g x ∂μ - ∫⁻ x, f x ∂μ ≤ ∫⁻ x, g x - f x ∂μ :=
  lintegral_sub_le' f g hf.aemeasurable

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

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

Разделы

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

Аффилиация

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