Theorems · Theorem · combinatorics

Finset.Nonempty.strong_induction

∀ {α : Type u_1} {p : (s : Finset α) → s.Nonempty → Prop},
  (∀ (a : α), p {a} ⋯) →
    (∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯) →
      ∀ ⦃s : Finset α⦄ (hs : s.Nonempty), p s hs

Suppose that, given objects defined on all nonempty strict subsets of any nontrivial finset s, one knows how to define an object on s. Then one can inductively define an object on all finsets, starting from singletons and iterating. TODO: Currently this can only be used to prove properties. Replace Finset.Nonempty.exists_eq_singleton_or_nontrivial with computational content in order to let p be Sort-valued.

Defined in

Mathlib.Data.Finset.Card

Cited by

0 results in Mathlib

Foundations

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