Theorems · Definition · combinatorics

Finset.strongDownwardInduction

{α : Type u_1} →
  {p : Finset α → Sort u_4} →
    {n : ℕ} →
      ((t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) →
        (s : Finset α) → s.card ≤ n → p s

Suppose that, given that p t can be defined on all supersets of s of cardinality less than n, one knows how to define p s. Then one can inductively define p s for all finsets s of cardinality less than n, starting from finsets of card n and iterating. This can be used either to define data, or to prove properties.

Defined in

Mathlib.Data.Finset.Card

Cited by

3 results in Mathlib

Foundations

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