English
Induction principle for finset families: to prove a property P for every Finset family 𝒜, it suffices to prove it for the empty family, for the singleton containing the empty set, and to show that if a holds for the nonMemberSubfamily and for the memberSubfamily of any 𝒜 with respect to any a, then it holds for 𝒜 itself.
Русский
Принцип индукции по семействам конечных множеств: чтобы доказать свойство P для каждого семейства Finset 𝒜, достаточно доказать его для пустого семейства, для единичного, содержащего пустое множество, и показать, что если свойство верно для подсемейства без a и подсемейства с a в отношении к 𝒜, то оно верно и для 𝒜.
LaTeX
$$$\\mathrm{MemberFamily\\;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 `ℬ` and `𝒞`, where `a` is an element of the
ground type and `𝒜` and `ℬ` are families of finsets not containing `a`.
Note that instead of giving `ℬ` and `𝒞`, the `subfamily` case gives you
`𝒜 = ℬ ∪ {s ∪ {a} | s ∈ 𝒞}`, so that `ℬ = 𝒜.nonMemberSubfamily` and `𝒞 = 𝒜.memberSubfamily`.
This is a way of formalising induction on `n` where `𝒜` is a finset family on `n` elements.
See also `Finset.family_induction_on.` -/
@[elab_as_elim]
theorem memberFamily_induction_on {p : Finset (Finset α) → Prop} (𝒜 : Finset (Finset α)) (empty : p ∅)
(singleton_empty : p {∅})
(subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (𝒜.nonMemberSubfamily a) → p (𝒜.memberSubfamily a) → p 𝒜) : p 𝒜 :=
by
set u := 𝒜.sup id
have hu : ∀ s ∈ 𝒜, s ⊆ u := fun s ↦ le_sup (f := id)
clear_value u
induction u using Finset.induction generalizing 𝒜 with
| empty =>
simp_rw [subset_empty] at hu
rw [← subset_singleton_iff', subset_singleton_iff] at hu
obtain rfl | rfl := hu <;> assumption
| insert a u _ ih =>
refine subfamily a (ih _ ?_) (ih _ ?_)
· simp only [mem_nonMemberSubfamily, and_imp]
exact fun s hs has ↦ (subset_insert_iff_of_notMem has).1 <| hu _ hs
· simp only [mem_memberSubfamily, and_imp]
exact fun s hs ha ↦ (insert_subset_insert_iff ha).1 <| hu _ hs
