English
A downward inductive principle: if P holds for all supersets of s with smaller cardinality than a fixed n, then P holds for s.
Русский
Уточнённый принцип сильной индукции по нисходящему направлению: если P выполняется для всех надмножеств s меньшей размерности, то P выполняется для s.
LaTeX
$$$\\text{strongDownwardInduction} \\, H \\, s \\, \\_ \\to \\text{p}(s)$$$
Lean4
/-- 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. -/
def strongDownwardInduction {p : Finset α → Sort*} {n : ℕ}
(H : ∀ t₁, (∀ {t₂ : Finset α}, #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁) : ∀ s : Finset α, #s ≤ n → p s
| s =>
H s fun {t} ht h =>
have := Finset.card_lt_card h
have : n - #t < n - #s := by omega
strongDownwardInduction H t ht
termination_by s => n - #s
