single_neg

Mathlib.Analysis.Normed.Lp.lpSpace

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

English

The single map is linear with respect to negation: single p i (−a) = − single p i a.

Русский

Картa single линейна по отношению к отрицанию: single p i (−a) = − single p i a.

LaTeX

$$$\text{lp.single } p i (-a) = -\text{lp.single } p i a.$$$

Lean4

@[simp]
protected theorem single_neg (p) (i : α) (a : E i) : lp.single p i (-a) = -lp.single p i a :=
  ext <| Pi.single_neg _ _

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

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

Разделы

Аффилиация

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