Theorems · Definition · combinatorics

Multiset.recOn

{α : Type u_1} →
  {C : Multiset α → Sort u_3} →
    (m : Multiset α) →
      C 0 →
        (C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)) →
          (∀ (a a' : α) (m : Multiset α) (b : C m),
              C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)) →
            C m

Companion to Multiset.rec with more convenient argument order.

Defined in

Mathlib.Data.Multiset.ZeroCons

Cited by

4 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound