proj_apply

Mathlib.NumberTheory.Dioph

URI: https://scilib.ai/kg/mathlib#Poly.proj_apply

English

The projection map satisfies proj i x = x i.

Русский

Проекция удовлетворяет $\mathrm{proj}(i)(x) = x(i)$.

LaTeX

$$$\mathrm{proj}\, i\, x = x(i)$$$

Lean4

@[simp]
theorem proj_apply (i : α) (x) : proj i x = x i :=
  rfl

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

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

Разделы

Аффилиация

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