setLIntegral_univ — Mathlib

English

For any f: α → ℝ≥0∞, the Lebesgue integral of f with respect to μ over the entire space equals the Lebesgue integral of f with respect to μ over the whole space treated as a restricted space.

Русский

Для функции f: α → ℝ≥0∞ интеграл Лебега по μ на всём пространстве равен интегралу по μ, ограниченному на всё пространство.

LaTeX

$$$$ \\int^-_{x \\in \\mathrm{univ}} f(x) \\\\ d\\mu \equiv \\int^-_{x} f(x) \\\\ d\\mu. $$$$

Lean4

theorem setLIntegral_univ (f : α → ℝ≥0∞) : ∫⁻ x in univ, f x ∂μ = ∫⁻ x, f x ∂μ := by rw [Measure.restrict_univ]

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