lintegral_indicator_one

Mathlib.MeasureTheory.Integral.Lebesgue.Basic

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

English

For measurable set s, the lintegral of indicator of 1 equals μ(s).

Русский

Для измеримого множества s линеграл индикатора единицы равен μ(s).

LaTeX

$$$$ \\int^- a, s.indicator 1(a) \\, d\\mu = \\mu(s). $$$$

Lean4

theorem lintegral_indicator_one {s : Set α} (hs : MeasurableSet s) : ∫⁻ a, s.indicator 1 a ∂μ = μ s := by simp [hs]

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

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

Разделы

Аффилиация

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