Path — Mathlib

English

Two paths are equal if all their components (edges and vertices) are equal; extensionality principle.

Русский

Два пути равны, если равны все их компоненты (вершины и ребра); принцип экстенсивности.

LaTeX

$$$\\forall f,g : X.Path(m), (\\forall i, f.arrow i = g.arrow i) \\Rightarrow f = g$$$

Lean4

/-- A path of length `n` in a simplicial set `X` is defined as a 1-truncated
path in the 1-truncation of `X`. -/
abbrev Path (X : SSet.{u}) (n : ℕ) :=
  truncation 1 |>.obj X |>.Path n

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