English
Induction principle for finset families: to prove a property for all 𝒜, it suffices to verify it for the empty family, the singleton {∅}, and that if it holds for ℬ and ℭ, then it holds for ℬ ∪ ℭ where ℬ and ℭ are families not containing a, accounting for the split into nonMemberSubfamily and memberSubfamily.
Русский
Индукция по семействам конечных множеств: чтобы доказать свойство для всех 𝒜, достаточно проверить его для пустого семейства, одного элемента {∅}, и что если свойство верно для ℬ и ℭ, то верно и для ℬ ∪ ℭ, где ℬ и ℭ не содержат a, с учётом разбиения на nonMemberSubfamily и memberSubfamily.
LaTeX
$$$\\mathrm{family\\_induction\\_on}: \\, \\forall p: Finset(Finset\\alpha)\\to Prop,\\ p\\emptyset\\land p\\{\\emptyset\\} \\land (\\forall a \\;\\forall \\mathcal{A}, p(\\mathcal{A}.nonMemberSubfamily a) \\to p(\\mathcal{A}.memberSubfamily a) \\to p\\mathcal{A}) \\to \\forall \\mathcal{A}, p\\mathcal{A}$$$
Lean4
/-- Induction principle for finset families. To prove a statement for every finset family,
it suffices to prove it for
* the empty finset family.
* the finset family which only contains the empty finset.
* `{s ∪ {a} | s ∈ 𝒜}` assuming the property for `𝒜` a family of finsets not containing `a`.
* `ℬ ∪ 𝒞` assuming the property for `ℬ` and `𝒞`, where `a` is an element of the ground type and
`ℬ`is a family of finsets not containing `a` and `𝒞` a family of finsets containing `a`.
Note that instead of giving `ℬ` and `𝒞`, the `subfamily` case gives you `𝒜 = ℬ ∪ 𝒞`, so that
`ℬ = {s ∈ 𝒜 | a ∉ s}` and `𝒞 = {s ∈ 𝒜 | a ∈ s}`.
This is a way of formalising induction on `n` where `𝒜` is a finset family on `n` elements.
See also `Finset.memberFamily_induction_on.` -/
@[elab_as_elim]
protected theorem family_induction_on {p : Finset (Finset α) → Prop} (𝒜 : Finset (Finset α)) (empty : p ∅)
(singleton_empty : p {∅})
(image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (𝒜.image <| insert a))
(subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜) : p 𝒜 :=
by
refine memberFamily_induction_on 𝒜 empty singleton_empty fun a 𝒜 h𝒜₀ h𝒜₁ ↦ subfamily a h𝒜₀ ?_
rw [← image_insert_memberSubfamily]
exact image_insert _ (by simp) h𝒜₁
