mkOfSucc_δ_gt — Mathlib

English

If j > i.succ, then mkOfSucc i ≫ δ_j = mkOfSucc i.succ.

Русский

Если j > i.succ, то mkOfSucc i ∘ δ_j = mkOfSucc i.succ.

LaTeX

$$$\\text{If } j > i.\\succ, \\ mkOfSucc i \\circ δ_j = mkOfSucc i.\\succ.$$$

Lean4

/-- If `i + 1 > j`, `mkOfSucc i ≫ δ j` is the morphism `⦋1⦌ ⟶ ⦋n⦌` that
sends `0` and `1` to `i + 1` and `i + 2`, respectively. -/
theorem mkOfSucc_δ_gt {n : ℕ} {i : Fin n} {j : Fin (n + 2)} (h : j < i.succ.castSucc) :
    mkOfSucc i ≫ δ j = mkOfSucc i.succ := by
  ext x
  simp only [δ, len_mk, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe, OrderEmbedding.toOrderHom_coe,
    Function.comp_apply, Fin.succAboveOrderEmb_apply]
  fin_cases x <;> rw [Fin.succAbove_of_le_castSucc]
  · rfl
  · exact Nat.le_of_lt_succ h
  · rfl
  · exact Nat.le_of_lt h

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