contractNth_apply_of_gt — Mathlib

English

If (j : Fin(n+1)) and (k : Fin n) with k > j, then contractNth j op g k equals g k.succ.

Русский

Если k > j, то contractNth j op g k = g k.succ.

LaTeX

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

Lean4

theorem contractNth_apply_of_gt (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (h : (j : ℕ) < k) :
    contractNth j op g k = g k.succ := by rw [contractNth, if_neg (not_lt_of_gt h), if_neg (Ne.symm <| ne_of_lt h)]

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