Path — Mathlib

English

A path in an (n+1)-truncated simplicial set X is defined as a 1-truncated path in the 1-truncation of X.

Русский

Путь в (n+1)-усеченном симпликальном множестве X определяется как 1-усечённый путь в 1-усечке X.

LaTeX

$$$\\mathrm{Path}(X,n) = \\mathrm{Path}_1(\\mathrm{trunc}(X))_n$$$

Lean4

/-- A path of length `m` in an `n + 1`-truncated simplicial set `X` is given by
the data of a `Path₁` structure on the further 1-truncation of `X`. -/
def Path {n : ℕ} (X : SSet.Truncated.{u} (n + 1)) (m : ℕ) :=
  trunc (n + 1) 1 |>.obj X |>.Path₁ m

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