English
Let f be a m-step path in a truncated simplicial set X, and let σ: X → Y be a morphism. For any j, l ∈ ℕ with j + l ≤ m, the j–l interval of the mapped path is the image under σ of the j–l interval of f; i.e., (f.map σ).interval j l h = (f.interval j l h).map σ.
Русский
Пусть f—путь длины m в усечённом симплициальном множестве X, и σ: X → Y—морфизм. Для любых j, l ∈ ℕ с j + l ≤ m, интервал длины j–l от образованного пути f σ совпадает с образом через σ интервала длины j–l самого пути f; то есть (f.map σ).interval j l h = (f.interval j l h).map σ.
LaTeX
$$$\forall m (X,Y) (f : \mathrm{Path}(X,m)) (\sigma : X \to Y) (j,l : \mathbb{N}) (h : j + l \le m),\ (f.map \sigma).\mathrm{interval} \, j \, l \, h = (f.\mathrm{interval} \, j \, l \, h).\mathrm{map} \sigma$$$
Lean4
theorem map_interval (f : Path X m) (σ : X ⟶ Y) (j l : ℕ) (h : j + l ≤ m) :
(f.map σ).interval j l h = (f.interval j l h).map σ :=
rfl
