Theorems · Theorem · combinatorics

Finset.cons_induction

∀ {α : Type u_3} {motive : Finset α → Prop},
  motive ∅ → (∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (Finset.cons a s h)) → ∀ (s : Finset α), motive s

Defined in

Mathlib.Data.Finset.Insert

Cited by

85 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound