Theorems · Theorem · combinatorics

Multiset.foldl_induction

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

Defined in

Mathlib.Data.Multiset.MapFold

Cited by

0 results in Mathlib

Foundations

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

Assumes

RightCommutative