eLpNorm'_exponent_zero

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.eLpNorm'_exponent_zero

English

There is a lattice structure on Lp with operations defined by a.e.-equivalence of sup/inf.

Русский

Существует решётка на Lp, операции над ней определяются через почти-eq равенство.

LaTeX

$$$\text{Lp}(E,p,\mu)$ is a lattice with sup/inf defined a.e.-equivalently.$$

Lean4

@[simp]
theorem eLpNorm'_exponent_zero {f : α → ε} : eLpNorm' f 0 μ = 1 := by rw [eLpNorm', div_zero, ENNReal.rpow_zero]

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

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

Разделы

Аффилиация

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