Theorems · Theorem · combinatorics

Multiset.Pi.cons_swap

∀ {α : Type u_1} [inst : DecidableEq α] {δ : α → Sort u_2} {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α}
  {f : (a : α) → a ∈ m → δ a},
  a ≠ a' →
    Multiset.Pi.cons (a' ::ₘ m) a b (Multiset.Pi.cons m a' b' f) ≍
      Multiset.Pi.cons (a ::ₘ m) a' b' (Multiset.Pi.cons m a b f)

Defined in

Mathlib.Data.Multiset.Pi

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEq