Truncated — Mathlib

English

Truncated(n) denotes the full subcategory of SimplexCategory consisting of objects with length at most n.

Русский

Truncated(n) обозначает полную подпорожцкую категорию SimplexCategory, состоящую из объектов с длиной не превосходящей n.

LaTeX

$$$\\mathrm{Truncated}(n) = \\mathrm{FullSubcategory}\\big(\\{ a:\\mathrm{SimplexCategory} \\mid a.len \\le n\\} \\big)$$$

Lean4

/-- The truncated simplex category. -/
def Truncated (n : ℕ) :=
  ObjectProperty.FullSubcategory fun a : SimplexCategory => a.len ≤ n

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