mkOfSucc_δ_lt — Mathlib

English

If i+1 < j, then mkOfSucc i ≫ δ_j = mkOfSucc i.castSucc.

Русский

Если i+1 < j, то mkOfSucc i ∘ δ_j = mkOfSucc i.castSucc.

LaTeX

$$$\\text{If } i+.1 < j, \\ mkOfSucc i \\circ δ_j = mkOfSucc i.castSucc.$$$

Lean4

/-- If `i + 1 < j`, `mkOfSucc i ≫ δ j` is the morphism `⦋1⦌ ⟶ ⦋n⦌` that
sends `0` and `1` to `i` and `i + 1`, respectively. -/
theorem mkOfSucc_δ_lt {n : ℕ} {i : Fin n} {j : Fin (n + 2)} (h : i.succ.castSucc < j) :
    mkOfSucc i ≫ δ j = mkOfSucc i.castSucc := by
  ext x
  fin_cases x
  · simp [δ, Fin.succAbove_of_castSucc_lt _ _ (Nat.lt_trans _ h)]
  · simp [δ, Fin.succAbove_of_castSucc_lt _ _ h]

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