English
Equality between strongInduction H s and the recursive construction holds.
Русский
Справедливость равенства между strongInduction H s и рекурсивной конструкцией.
LaTeX
$$$\\text{strongInduction}(H)\\,s = H\\,s(\\lambda t, \\_ => \\text{strongInduction}(H)(t))$$$
Lean4
/-- Suppose that, given objects defined on all nonempty strict subsets of any nontrivial finset `s`,
one knows how to define an object on `s`. Then one can inductively define an object on all finsets,
starting from singletons and iterating.
TODO: Currently this can only be used to prove properties.
Replace `Finset.Nonempty.exists_eq_singleton_or_nontrivial` with computational content
in order to let `p` be `Sort`-valued. -/
@[elab_as_elim]
protected theorem strong_induction {p : ∀ s, s.Nonempty → Prop} (h₀ : ∀ a, p { a } (singleton_nonempty _))
(h₁ : ∀ ⦃s⦄ (hs : s.Nontrivial), (∀ t ht, t ⊂ s → p t ht) → p s hs.nonempty) : ∀ ⦃s : Finset α⦄ (hs), p s hs
| s, hs => by
obtain ⟨a, rfl⟩ | hs := hs.exists_eq_singleton_or_nontrivial
· exact h₀ _
· refine h₁ hs fun t ht hts ↦ ?_
have := card_lt_card hts
exact ht.strong_induction h₀ h₁
termination_by s => #s
