toLp_one_eq_toL1

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

← MathLib Explorer

English

For any element a in a preorder, le(a,a) holds (reflexivity).

Русский

Для любой позиции в предорде le(a,a) истинно (рефлексивность).

LaTeX

$$$$a \\le a.$$$$

Lean4

theorem toLp_one_eq_toL1 (f : α →ₛ E) (hf : Integrable f μ) :
    (Lp.simpleFunc.toLp f (memLp_one_iff_integrable.2 hf) : α →₁[μ] E) = hf.toL1 f :=
  rfl

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

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

Разделы

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

Аффилиация

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