δ_comp_σ_of_gt' — Mathlib

English

A further match of δ and σ identities in a GT context.

Русский

Дальнейшее соответствие тождений δ и σ в контексте GT.

LaTeX

$$$X.\delta_j \circ X.\sigma_i = X.\delta_i \circ X.\sigma_j$$$

Lean4

@[reassoc]
theorem δ_comp_σ_of_gt' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
    X.σ j ≫ X.δ i =
      X.δ (i.pred fun (hi : i = 0) => by simp only [Fin.not_lt_zero, hi] at H) ≫
        X.σ (j.castLT ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le H i.is_le))) :=
  by
  dsimp [δ, σ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]

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