English
Induction up to a finite set S: if S is finite, and S0 ⊆ S with C(S0) and for all s ⊂ S, C(s) → ∃ a ∈ S\\s with C(insert a s), then C(S).
Русский
Индукция на конечном множестве S: если S конечно и существует базовый подмножество S0 ⊆ S с C(S0), а для любого s ⊂ S верно: C(s) ⇒ существование a ∈ S\\s с C(S ∪ {a})? Тогда C(S).
LaTeX
$$$S\\text{ finite} \\Rightarrow C(S_0) \\Rightarrow (\\forall s \\subset S, C(s) \\Rightarrow \\exists a \\in S \\setminus s, C(s \\cup \\{a\\})) \\Rightarrow C(S)$$$
Lean4
/-- Induction up to a finite set `S`. -/
theorem induction_to {C : Set α → Prop} {S : Set α} (h : S.Finite) (S0 : Set α) (hS0 : S0 ⊆ S) (H0 : C S0)
(H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)) : C S :=
by
have : Finite S := Finite.to_subtype h
have : Finite { T : Set α // T ⊆ S } := Finite.of_equiv (Set S) (Equiv.Set.powerset S).symm
rw [← Subtype.coe_mk (p := (· ⊆ S)) _ le_rfl]
rw [← Subtype.coe_mk (p := (· ⊆ S)) _ hS0] at H0
refine Finite.to_wellFoundedGT.wf.induction_bot' (fun s hs hs' ↦ ?_) H0
obtain ⟨a, ⟨ha1, ha2⟩, ha'⟩ := H1 s (ssubset_of_ne_of_subset hs s.2) hs'
exact ⟨⟨insert a s.1, insert_subset ha1 s.2⟩, Set.ssubset_insert ha2, ha'⟩
