Theorems · Theorem · combinatorics

Finset.induction_on

∀ {α : Type u_3} {motive : Finset α → Prop} [inst : DecidableEq α] (s : Finset α),
  motive ∅ → (∀ (a : α) (s : Finset α), a ∉ s → motive s → motive (insert a s)) → motive s

To prove a proposition about an arbitrary Finset α, it suffices to prove it for the empty Finset, and to show that if it holds for some Finset α, then it holds for the Finset obtained by inserting a new element.

Defined in

Mathlib.Data.Finset.Insert

Cited by

167 results in Mathlib

Foundations

Depth 60 from the axioms, rests on 827 definitions · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq