map_ι_liftPath — Mathlib

English

The map from the lifted path back down via A.ι is the original path p.

Русский

Отображение пути, полученного после подъёма, через A.ι даёт исходный путь p.

LaTeX

$$$(A.liftPath p hp_0 hp_1).map(A.ι) = p$$$

Lean4

@[simp]
theorem map_ι_liftPath {X : SSet.{u}} (A : X.Subcomplex) {n : ℕ} (p : Path X n) (hp₀ : ∀ j, p.vertex j ∈ A.obj _)
    (hp₁ : ∀ j, p.arrow j ∈ A.obj _) : (A.liftPath p hp₀ hp₁).map A.ι = p :=
  rfl

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