stdSimplexHomeomorphUnitInterval_one

English

There is a canonical homeomorphism between the standard simplex and the unit interval; specifically, the image of the vertex corresponding to the first coordinate under this homeomorphism is the endpoint 1 of the unit interval.

Русский

Существует канонический гомеоморфизм между стандартным симплексом и единичным отрезком; в частности, вершина, соответствующая первой координате, отображается в точку 1 единичного отрезка.

LaTeX

$$$\operatorname{stdSimplexHomeomorphUnitInterval}(\operatorname{vertex}(1)) = 1$$$

Lean4

@[simp]
theorem stdSimplexHomeomorphUnitInterval_one : stdSimplexHomeomorphUnitInterval ⟨_, single_mem_stdSimplex _ 1⟩ = 1 :=
  rfl

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