insertNth_binop — Mathlib

English

Inserts of a pointwise binary operation distribute over the insertion at index i.

Русский

Вставка бинарной операции по индексу i распределяется по вставке.

LaTeX

$$$$ (i.insertNth (op i x y) (\lambda j, op \_ (p j) (q j))) = (\lambda j, op j (i.insertNth x p j) (i.insertNth y q j)) $$$$

Lean4

theorem insertNth_binop (op : ∀ j, α j → α j → α j) (i : Fin (n + 1)) (x y : α i) (p q : ∀ j, α (i.succAbove j)) :
    (i.insertNth (op i x y) fun j ↦ op _ (p j) (q j)) = fun j ↦ op j (i.insertNth x p j) (i.insertNth y q j) :=
  insertNth_eq_iff.2 <| by unfold removeNth; simp

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