contractNth_apply_of_ne — Mathlib

English

If j.val ≠ k.val, then contractNth j op g k equals g(j.succAbove k).

Русский

Если значения j и k различны, то contractNth j op g k = g(j.succAbove k).

LaTeX

$$$\\text{contractNth}(j, op, g)(k) = g(j.conn\\succAbove k) \\quad\\text{when } j \\neq k$$$

Lean4

theorem contractNth_apply_of_ne (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n)
    (hjk : (j : ℕ) ≠ k) : contractNth j op g k = g (j.succAbove k) :=
  by
  rcases lt_trichotomy (k : ℕ) j with (h | h | h)
  · rwa [j.succAbove_of_castSucc_lt, contractNth_apply_of_lt]
    · rwa [Fin.lt_iff_val_lt_val]
  · exact False.elim (hjk h.symm)
  · rwa [j.succAbove_of_le_castSucc, contractNth_apply_of_gt]
    · exact Fin.le_iff_val_le_val.2 (le_of_lt h)

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