stdSimplexHomeomorphUnitInterval_zero

Mathlib.Analysis.Convex.StdSimplex

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

English

The image under stdSimplexEquivIcc of the left endpoint is 0.

Русский

Образ левого конца под stdSimplexEquivIcc равен 0.

LaTeX

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

Lean4

@[simp]
theorem stdSimplexHomeomorphUnitInterval_zero : stdSimplexHomeomorphUnitInterval ⟨_, single_mem_stdSimplex _ 0⟩ = 0 :=
  rfl

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

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

Разделы

Аффилиация

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