δ_comp_σ_of_gt' — Mathlib

English

If H: j.succ < i, then δ_i ≫ σ_j equals a modified σ with j.castLT and δ_i.pred depending on H.

Русский

При условии H: j.succ < i выполняется δ_i ≫ σ_j = σ_{j.castLT(...)} ≫ δ_{i.pred(...)}.

LaTeX

$$$\\delta i \\circ \\sigma j = \\sigma( j.castLT ( (add\\_lt\\_add\\_iff\\_right 1).mp (lt\_of\_lt\_of\_le H i.is\_le) )) \\circ \\delta ( i.pred ( \\lambda h: i = 0 => ... ))$$$

Lean4

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

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