instNormOneClass

Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

URI: https://scilib.ai/kg/mathlib#TrivSqZeroExt.instNormOneClass

English

A second instance provides a bounded scalar action on tsze by using the product space.

Русский

Вторая инстанция задаёт ограниченное действие скаляра на tsze через произведение.

LaTeX

$$$\\text{IsBoundedSMul } S (WithLp 1 \\,(R \\times M))$$$

Lean4

instance [NormOneClass R] : NormOneClass (tsze R M) where
  norm_one := by rw [norm_def, fst_one, snd_one, norm_zero, norm_one, add_zero]

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

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

Разделы

Аффилиация

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