lintegral_mono

Mathlib.MeasureTheory.Function.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEEqFun.lintegral_mono

English

If f ≤ g almost everywhere, then lintegral f ≤ lintegral g.

Русский

Если f ≤ g почти повсеместно, то лин интеграл f ≤ лин интеграл g.

LaTeX

$$lintegral_mono {f g : α →ₘ[μ] ℝ≥0∞} : f ≤ g → lintegral f ≤ lintegral g$$

Lean4

theorem lintegral_mono {f g : α →ₘ[μ] ℝ≥0∞} : f ≤ g → lintegral f ≤ lintegral g :=
  induction_on₂ f g fun _f _ _g _ hfg => lintegral_mono_ae hfg

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

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

Разделы

Аффилиация

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