noncommFoldr_cons — Mathlib

English

For a multiset s and an element a, the fold over a :: s equals f(a, noncommFoldr(s, h', b)) with an appropriate commutativity witness h and h'.

Русский

Для мультиcета s и элемента a свертка по a ∪ s равна f(a, свёртке по s с подходящим доказательством коммутативности h').

LaTeX

$$$\\mathrm{noncommFoldr}(f,(\\mathrm{cons}\ a\ s))\\; h\\; b = f\\ a\\; (\\mathrm{noncommFoldr}(f\ s\\, h'\\, b)).$$$

Lean4

theorem noncommFoldr_cons (s : Multiset α) (a : α) (h h') (b : β) :
    noncommFoldr f (a ::ₘ s) h b = f a (noncommFoldr f s h' b) :=
  by
  induction s using Quotient.inductionOn
  simp

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