Theorems · Theorem · combinatorics

Multiset.rel_cons_left

∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {a : α} {as : Multiset α} {bs : Multiset β},
  Multiset.Rel r (a ::ₘ as) bs ↔ ∃ b bs', r a b ∧ Multiset.Rel r as bs' ∧ bs = b ::ₘ bs'

Defined in

Mathlib.Data.Multiset.ZeroCons

Cited by

3 results in Mathlib

Foundations

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