Theorems · Theorem · combinatorics

Multiset.foldr_induction

∀ {α : Type u_1} (f : α → α → α) [inst : LeftCommutative f] (x : α) (p : α → Prop) (s : Multiset α),
  (∀ (a b : α), p a → p b → p (f a b)) → p x → (∀ a ∈ s, p a) → p (Multiset.foldr f x s)

Defined in

Mathlib.Data.Multiset.MapFold

Cited by

2 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound

Assumes

LeftCommutative