coeFn_zero

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.simpleFunc.coeFn_zero

English

The zero simple function in Lp corresponds almost everywhere to the zero function.

Русский

Нулевая простая функция в Lp эквивалентна нулевой функции почти везде.

LaTeX

$$$(0 : Lp.simpleFunc\ G\ p\ μ) =ᵐ[μ] (0 : α \to G)$$$

Lean4

theorem coeFn_zero : (0 : Lp.simpleFunc G p μ) =ᵐ[μ] (0 : α → G) :=
  Lp.coeFn_zero _ _ _

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

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

Разделы

Аффилиация

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