instIsBoundedSMulSubtypePreLpMemAddSubgroup

Mathlib.Analysis.Normed.Lp.lpSpace

URI: https://scilib.ai/kg/mathlib#lp.instIsBoundedSMulSubtypePreLpMemAddSubgroup

English

If 1 ≤ p, then the scalar multiplication action by 𝕜 on lp E p is bounded.

Русский

Если 1 ≤ p, то действие скаляра 𝕜 на lp(E,p) ограничено (bounded).

LaTeX

$$$\\text{IsBoundedSMul } 𝕜 (lp E p)\\quad\\text{when } 1\\le p$$$

Lean4

instance [Fact (1 ≤ p)] : IsBoundedSMul 𝕜 (lp E p) :=
  IsBoundedSMul.of_norm_smul_le <| norm_const_smul_le (zero_lt_one.trans_le <| Fact.out).ne'

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

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

Разделы

Аффилиация

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