Theorems · Theorem · combinatorics

Finset.strongDownwardInductionOn_eq

∀ {α : Type u_1} {n : ℕ} {p : Finset α → Sort u_4} (s : Finset α)
  (H : (t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁),
  (fun a => s.strongDownwardInductionOn H a) = H s fun {t} ht x => t.strongDownwardInductionOn H ht

Defined in

Mathlib.Data.Finset.Card

Cited by

0 results in Mathlib

Foundations

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