Theorems · Definition · combinatorics

Finset.strongDownwardInductionOn

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

Analogue of strongDownwardInduction with order of arguments swapped.

Defined in

Mathlib.Data.Finset.Card

Cited by

2 results in Mathlib

Foundations

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