setLIntegral_one

Mathlib.MeasureTheory.Integral.Lebesgue.Basic

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

English

The lintegral over any set of the constant function 1 equals the measure of that set.

Русский

Линтеграл единицы по множеству равен мере множества.

LaTeX

$$$$ \int^- x in s, 1 \partial \mu = \mu(s). $$$$

Lean4

theorem setLIntegral_one (s) : ∫⁻ _ in s, 1 ∂μ = μ s := by rw [setLIntegral_const, one_mul]

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

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

Разделы

Аффилиация

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