English
The strong induction operator on Finsets yields equality with the explicit recursive definition: strongInduction H s = H s (fun t _ => strongInduction H t).
Русский
Оператор сильной индукции на конечных множествах эквивалентен явному рекурсивному определению: strongInduction H s = H s (функция, отображающая t в strongInduction H t).
LaTeX
$$$\\text{strongInduction}(H)\\,s = H\\,s\\bigl(\\lambda t, \\_ => \\text{strongInduction}(H)\\,t\\bigr)$$$
Lean4
/-- Suppose that, given objects defined on all strict subsets of any finset `s`, one knows how to
define an object on `s`. Then one can inductively define an object on all finsets, starting from
the empty set and iterating. This can be used either to define data, or to prove properties. -/
def strongInduction {p : Finset α → Sort*} (H : ∀ s, (∀ t ⊂ s, p t) → p s) : ∀ s : Finset α, p s
| s =>
H s fun t h =>
have : #t < #s := card_lt_card h
strongInduction H t
termination_by s => #s
