Theorems · Theorem · combinatorics

Multiset.Pi.cons_ne

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

Defined in

Mathlib.Data.Multiset.Pi

Cited by

5 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

DecidableEq