ite_eq_mem_stdSimplex — Mathlib

English

The function that takes value 1 at index i and 0 elsewhere belongs to stdSimplex 𝕜 ι.

Русский

Функция, принимающая значение 1 в индексе i и 0 в остальных местах, принадлежит stdSimplex 𝕜 ι.

LaTeX

$$$(\mathrm{Pi.single}\ i\ 1) \in \mathrm{stdSimplex}_{\mathbb{k}}(\iota)$$$

Lean4

theorem ite_eq_mem_stdSimplex (i : ι) : (if i = · then (1 : 𝕜) else 0) ∈ stdSimplex 𝕜 ι := by
  simpa only [@eq_comm _ i, ← Pi.single_apply] using single_mem_stdSimplex 𝕜 i

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