lpInftySubring

Mathlib.Analysis.Normed.Lp.lpSpace

URI: https://scilib.ai/kg/mathlib#lpInftySubring

← MathLib Explorer

English

If f ∈ Memℓp, then star f ∈ Memℓp.

Русский

Если f ∈ Memℓp, то star f ∈ Memℓp.

LaTeX

$$$Mem\\ell p (star f) p$$$

Lean4

/-- The `𝕜`-subring of elements of `∀ i : α, B i` whose `lp` norm is finite. This is `lp E ∞`,
with extra structure. -/
def _root_.lpInftySubring : Subring (PreLp B) :=
  { lp B ∞ with
    carrier := {f | Memℓp f ∞}
    one_mem' := one_memℓp_infty
    mul_mem' := Memℓp.infty_mul }

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

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

Разделы

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

Аффилиация

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