stdSimplexEquivIcc_one

Mathlib.Analysis.Convex.StdSimplex

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

English

The image of the right endpoint under the standard simplex to Icc correspondence is 1.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem stdSimplexEquivIcc_one : stdSimplexEquivIcc 𝕜 ⟨_, single_mem_stdSimplex 𝕜 1⟩ = 1 :=
  rfl

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

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

Разделы

Аффилиация

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