English
There is a canonical coe from the elements of the topological simplex to functions on the index set, identifying each point with its coordinate function.
Русский
Существует каноническое включение из элементов toTopObj(x) в функции на множество индексов, отождествляющее каждую точку с ее координатной функцией.
LaTeX
$$$(x^{\\mathrm{top}})^{\\mathrm{Elem}} \\hookrightarrow (\\mathrm{ToType}(x) \\to \\mathbb{R}_{\\ge 0})$ via $f \\mapsto (f : \\mathrm{ToType}(x) \\to \\mathbb{R}_{\\ge 0})$$$
Lean4
instance (x : SimplexCategory) : CoeFun x.toTopObj fun _ => ToType x → ℝ≥0 :=
⟨fun f => (f : ToType x → ℝ≥0)⟩
