instIsScalarTowerSubtypePreLpMemAddSubgroup

Mathlib.Analysis.Normed.Lp.lpSpace

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

English

The subtype of lp E p inherits a scalar-tower structure 𝕜' → 𝕜 → Subtype.

Русский

Подмножество lp E p наследует структуру торов скаляров 𝕜' → 𝕜 → Subtype.

LaTeX

$$$IsScalarTower 𝕜' 𝕜 (Subtype (f\\in lp E p))$$$

Lean4

instance [SMul 𝕜' 𝕜] [∀ i, IsScalarTower 𝕜' 𝕜 (E i)] : IsScalarTower 𝕜' 𝕜 (lp E p) :=
  ⟨fun _ _ _ => Subtype.ext <| smul_assoc _ _ _⟩

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

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

Разделы

Аффилиация

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