fac_aux₃ — Mathlib

English

A strict Segal simplicial set is 2-coskeletal; equivalently, it satisfies a pointwise right Kan extension condition for the inclusion of the 2-skeleton.

Русский

Строгое сегалово симпликальное множество 2-коскелетично; эквивалентно выполнению условия точного правого кан-расширения для включения 2-скелета.

LaTeX

$$$ \\text{isPointwiseRightKanExtensionAt}(X, 2) \\text{ holds for } X \\text{ strictSegal}$$$

Lean4

theorem fac_aux₃ {n : ℕ} (s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
    (x : s.pt) (φ : ⦋1⦌ ⟶ ⦋n⦌) : X.map φ.op (lift sx s x) = s.π.app (strArrowMk₂ φ) x :=
  by
  obtain ⟨i, j, hij, rfl⟩ : ∃ i j hij, φ = mkOfLe i j hij :=
    ⟨φ.toOrderHom 0, φ.toOrderHom 1, φ.toOrderHom.monotone (by decide), Hom.ext_one_left _ _ rfl rfl⟩
  exact fac_aux₂ _ _ _ _ _ _ (by cutsat)

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