Theorems · Theorem · combinatorics

Multiset.rel_cons_right

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

Defined in

Mathlib.Data.Multiset.ZeroCons

Cited by

2 results in Mathlib

Foundations

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