stdSimplexEquivIcc_zero

Mathlib.Analysis.Convex.StdSimplex

URI: https://scilib.ai/kg/mathlib#stdSimplexEquivIcc_zero

English

The image of the left endpoint under the standard simplex to Icc correspondence is 0.

Русский

Образ левой границы в эквивалентности стандартного симплекса и Icc равен 0.

LaTeX

$$$stdSimplexEquivIcc\ 𝕜(\langle Pi.single 0 1, \dots \rangle) = 0$$$

Lean4

@[simp]
theorem stdSimplexEquivIcc_zero : stdSimplexEquivIcc 𝕜 ⟨_, single_mem_stdSimplex 𝕜 0⟩ = 0 :=
  rfl

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

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

Разделы

Аффилиация

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