contractNth_apply_of_lt — Mathlib

English

If k < j, then contractNth j op g at k equals g at castSucc k.

Русский

Если k < j, то contractNth j op g при аргументе k равно g при CastSucc k.

LaTeX

$$$\\text{contractNth}(j, op, g)(k) = g(\\text{castSucc }k) \\quad\\text{when } (k:\\mathbb{N}) < j$$$

Lean4

theorem contractNth_apply_of_lt (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n) (h : (k : ℕ) < j) :
    contractNth j op g k = g (Fin.castSucc k) :=
  if_pos h

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