insertNth_apply_below — Mathlib

English

If j < i, then (insertNth i x p) j equals p(j.castPred) (up to the appropriate transport).

Русский

Если j < i, то (insertNth i x p) j равен p(j.castPred) с нужной передачей типа.

LaTeX

$$If {h: j < i}, (insertNth i x p) j = succAbove_castPred_of_lt i j h ▸ p j.castPred$$

Lean4

theorem insertNth_apply_below {i j : Fin (n + 1)} (h : j < i) (x : α i) (p : ∀ k, α (i.succAbove k)) :
    i.insertNth x p j = succAbove_castPred_of_lt _ _ h ▸ (p <| j.castPred _) := by
  rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_lt h), dif_pos h]

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