single_apply_ne

Mathlib.Analysis.Normed.Lp.lpSpace

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

English

If j ≠ i, then the i-th single evaluates to zero at index j.

Русский

Если j ≠ i, то i-я координатная функция равна нулю на индексе j.

LaTeX

$$$\text{lp.single } p i a (j) = 0 \quad\text{for } j \neq i.$$$

Lean4

protected theorem single_apply_ne (p) (i : α) (a : E i) {j : α} (hij : j ≠ i) : lp.single p i a j = 0 :=
  Pi.single_eq_of_ne hij _

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

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

Разделы

Аффилиация

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