Theorems · Definition · combinatorics

Multiset.Rel.casesOn

∀ {α : Type u_1} {β : Type v} {r : α → β → Prop}
  {motive : (a : Multiset α) → (a_1 : Multiset β) → Multiset.Rel r a a_1 → Prop} {a : Multiset α} {a_1 : Multiset β}
  (t : Multiset.Rel r a a_1),
  motive 0 0 ⋯ →
    (∀ {a : α} {b : β} {as : Multiset α} {bs : Multiset β} (a_2 : r a b) (a_3 : Multiset.Rel r as bs),
        motive (a ::ₘ as) (b ::ₘ bs) ⋯) →
      motive a a_1 t

Defined in

Mathlib.Data.Multiset.ZeroCons

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound