English
Induction on finite sets with subset-controlled insertion: to prove motive for s, it suffices to assume motive for t ⊆ s and then prove motive for insert a t when a ∈ s and a ∉ t.
Русский
Индукция по подмножествам с контролем над вставкой: чтобы доказать motive для s, достаточно предположить motive для t ⊆ s и затем доказать motive (insert a t) при a ∈ s и a ∉ t.
LaTeX
$$$ \\forall s \\; hs : s.Finite,\\ motive\\emptyset \\Rightarrow (\\forall {a t}, a \\in s \\rightarrow t \\subseteq s \\\\ a \\notin t \\\\ motive t (hs.subset hts) \\Rightarrow motive (insert a t) ((hs.subset hts).insert a)) \\Rightarrow motive s hs $$$
Lean4
/-- Induction principle for finite sets: To prove a property `C` of a finite set `s`, it's enough
to prove for the empty set and to prove that `C t → C ({a} ∪ t)` for all `t ⊆ s`.
This is analogous to `Finset.induction_on'`. See also `Set.Finite.induction_on` for the version
requiring `C t → C ({a} ∪ t)` for all `t`. -/
@[elab_as_elim]
theorem induction_on_subset {motive : ∀ s : Set α, s.Finite → Prop} (s : Set α) (hs : s.Finite)
(empty : motive ∅ finite_empty)
(insert :
∀ {a t},
a ∈ s → ∀ hts : t ⊆ s, a ∉ t → motive t (hs.subset hts) → motive (insert a t) ((hs.subset hts).insert a)) :
motive s hs :=
by
refine
Set.Finite.induction_on (motive := fun t _ => ∀ hts : t ⊆ s, motive t (hs.subset hts)) s hs (fun _ => empty) ?_ .rfl
intro a s has _ hCs haS
rw [insert_subset_iff] at haS
exact insert haS.1 haS.2 has (hCs haS.2)
