memLp_top

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

← MathLib Explorer

English

Every simple function lies in L^∞(μ).

Русский

Каждая простая функция принадлежит L^∞(μ).

LaTeX

$$$f \\in L^{\\infty}(\\mu)$$$

Lean4

theorem memLp_top (f : α →ₛ E) (μ : Measure α) : MemLp f ∞ μ :=
  let ⟨C, hfC⟩ := f.exists_forall_norm_le
  memLp_top_of_bound f.aestronglyMeasurable C <| Eventually.of_forall hfC

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

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

Разделы

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

Аффилиация

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