single_apply_self

Mathlib.Analysis.Normed.Lp.lpSpace

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

English

The map that selects the i-th coordinate (single i) is an isometry when p≥1.

Русский

Отображение, выбирающее i-ю координату (single i), является изометрией при p≥1.

LaTeX

$$$\text{Isometry}(\text{lp.single } p i)\quad\text{for } p \ge 1.$$$

Lean4

protected theorem single_apply_self (p) (i : α) (a : E i) : lp.single p i a i = a :=
  Pi.single_eq_same _ _

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

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

Разделы

Аффилиация

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