contractNth_apply_of_eq — Mathlib

English

If k.val = j, then contractNth j op g k equals op(g castSucc k, g k.succ).

Русский

Если k равен j, то contractNth j op g k = op(g castSucc k, g k.succ).

LaTeX

$$$\\text{contractNth}(j, op, g)(k) = op(g(\\text{castSucc }k), g(k.succ)) \\quad\\text{when } k = j$$$

Lean4

theorem contractNth_apply_of_eq (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (h : (k : ℕ) = j) :
    contractNth j op g k = op (g (Fin.castSucc k)) (g k.succ) :=
  by
  have : ¬(k : ℕ) < j := not_lt.2 (le_of_eq h.symm)
  rw [contractNth, if_neg this, if_pos h]

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