toTopObj — Mathlib

English

For each x in SimplexCategory, the topological simplex toTopObj(x) is the set of nonnegative functions on the index set with sum equal to 1.

Русский

Для каждого x из SimplexCategory топологический симплекс toTopObj(x) есть множество функций f: ToType x → ℝ≥0 с условием ∑ f(i) = 1.

LaTeX

$$$x^{\\mathrm{top}} = \\{ f : \\mathrm{ToType}(x) \\to \\mathbb{R}_{\\ge 0} \\mid \\sum_i f(i) = 1 \\}$$$

Lean4

/-- The topological simplex associated to `x : SimplexCategory`.
  This is the object part of the functor `SimplexCategory.toTop`. -/
def toTopObj (x : SimplexCategory) :=
  {f : ToType x → ℝ≥0 | ∑ i, f i = 1}

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