lintegral_eq_zero_of_ae_eq_zero

Mathlib.MeasureTheory.Integral.Lebesgue.Basic

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

English

If f =ᵃᵉ[μ] 0, then lintegral μ f = 0.

Русский

Если f = ae 0 по μ, то линегральный интеграл μ f равен нулю.

LaTeX

$$$\\int f \\, d\\mu = 0$$$

Lean4

theorem lintegral_eq_zero_of_ae_eq_zero {f : α → ℝ≥0∞} (h : f =ᵐ[μ] 0) : ∫⁻ a, f a ∂μ = 0 :=
  (lintegral_congr_ae h).trans lintegral_zero

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

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

Разделы

Аффилиация

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