lintegral_norm_eq_lintegral_edist

Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

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

← MathLib Explorer

English

The lintegral of the zero function is zero: ∫ ‖0‖ dμ = 0.

Русский

Линтеграл нулевой функции равен нулю: ∫ ‖0‖ dμ = 0.

LaTeX

$$$ \\int^-_\\alpha \\|0\\|_{\\varepsilon''} \\, d\\mu = 0 $$$

Lean4

theorem lintegral_norm_eq_lintegral_edist (f : α → β) : ∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ = ∫⁻ a, edist (f a) 0 ∂μ := by
  simp only [ofReal_norm_eq_enorm, edist_zero_eq_enorm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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