fac_aux₁ — Mathlib

English

A technical lemma used in the construction of a pointwise right Kan extension; this expresses a compatibility between a lift and a cone map at a fixed vertex.

Русский

Техническая лемма для построения точного правого кан-расширения, выражающая совместимость подъёма и конусной карты в фиксированной вершине.

LaTeX

$$$ \\text{fac\_aux}_1 \\]$$$

Lean4

theorem fac_aux₁ {n : ℕ} (s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
    (x : s.pt) (i : ℕ) (hi : i < n) :
    X.map (mkOfSucc ⟨i, hi⟩).op (lift sx s x) = s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩)) x :=
  by
  dsimp [lift]
  rw [spineToSimplex_arrow]
  rfl

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