integral_indicator_one — Mathlib

English

Let s ⊆ X be measurable. Then the Bochner integral of the function x ↦ s.indicator 1 x with respect to μ equals μ.real s.

Русский

Пусть s ⊆ X измеримо. Тогда интеграл по мере μ функции x ↦ s.indicator(1) равен μ.real(s).

LaTeX

$$$$ \\int_X \\mathbf{1}_s(x) \\; d\\mu(x) = \\mu_{\\mathbb{R}}(s). $$$$

Lean4

@[simp]
theorem integral_indicator_one ⦃s : Set X⦄ (hs : MeasurableSet s) : ∫ x, s.indicator 1 x ∂μ = μ.real s :=
  (integral_indicator_const 1 hs).trans ((smul_eq_mul ..).trans (mul_one _))

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