Theorems · Theorem · combinatorics

Fin.insertNth_binop

∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (op : (j : Fin (n + 1)) → α j → α j → α j) (i : Fin (n + 1)) (x y : α i)
  (p q : (j : Fin n) → α (i.succAbove j)),
  (i.insertNth (op i x y) fun j => op (i.succAbove j) (p j) (q j)) = fun j =>
    op j (i.insertNth x p j) (i.insertNth y q j)

Defined in

Mathlib.Data.Fin.Tuple.Basic

Cited by

4 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound