zero_lintegral

Mathlib.MeasureTheory.Function.SimpleFunc

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.zero_lintegral

English

For every simple function f, the lintegral with respect to μ of the zero function is zero.

Русский

Для любой простой функции f лине́граль по мере μ нулевой функции равен нулю.

LaTeX

$$$ (0 : α \\toₛ ℝ_{≥0}^{∞}).lintegral μ = 0 $$$

Lean4

@[simp]
theorem zero_lintegral : (0 : α →ₛ ℝ≥0∞).lintegral μ = 0 :=
  LinearMap.ext_iff.1 lintegralₗ.map_zero μ

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

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

Разделы

Аффилиация

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