Theorems · Theorem · combinatorics

Multiset.rel_iff

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

Defined in

Mathlib.Data.Multiset.ZeroCons

Cited by

2 results in Mathlib

Foundations

Depth 16 from the axioms · uses Quot.sound