δ_comp_σ_of_gt' — Mathlib

English

Variant of the previous with refined indexing (gt' form).

Русский

Вариант предыдущего с уточнённой индексацией (gt' форма).

LaTeX

$$$\delta_{i} \circ \sigma_{j.castSucc} = \sigma_{\mathrm{castLT}(\dots)} \circ \delta_{i}$$$

Lean4

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

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