ring

Mathlib.Analysis.Normed.Lp.lpSpace

URI: https://scilib.ai/kg/mathlib#PreLp.ring

English

For hp ≥ 1 (or Fact hp), the scalar multiplication on lp E p is bounded.

Русский

Для hp ≥ 1 (или Fact hp) скалярное умножение на lp E p ограничено.

LaTeX

$$$IsBoundedSMul 𝕜 (lp B p)$$$

Lean4

instance _root_.PreLp.ring : Ring (PreLp B) :=
  Pi.ring

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

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

Разделы

Аффилиация

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