map — Mathlib

English

Maps of simplicial sets induce maps on paths: given a path f in X and a map σ: X → Y, there is a corresponding path f mapped to Y of the same length.

Русский

Изобразимости симпликальных множеств порождают отображения путей: имея путь f в X и отображение σ: X → Y, существует соответствующий путь в Y того же длины.

LaTeX

$$$(f,\sigma) \mapsto f^{\sigma} \in \mathrm{Path}(Y,n)$$$

Lean4

/-- Maps of simplicial sets induce maps of paths in a simplicial set. -/
def map (f : Path X n) (σ : X ⟶ Y) : Path Y n :=
  Truncated.Path.map f ((truncation 1).map σ)

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