English
Induction principle for finset families: to prove a property for all Finset families, it suffices to prove it for the empty family, the singleton {∅}, and that if it holds for the nonMemberSubfamily and the memberSubfamily of 𝒜 with respect to a, then it holds for 𝒜.
Русский
Принцип индукции по семействам Finset: чтобы доказать свойство для всех 𝒜, достаточно доказать его для пустого семейства, для {∅}, и что если свойство верно для nonMemberSubfamily и для memberSubfamily 𝒜 по отношению к a, то оно верно и для 𝒜.
LaTeX
$$$\\mathrm{memberFamily\\_induction\\_on}: \\, \\forall p: Finset(Finset\\alpha)\\to Prop,\\ p\\emptyset\\land p\\{\\emptyset\\} \\land (\\forall a\\;\\forall 𝒜,\\ p(𝒜.nonMemberSubfamily a) \\to p(𝒜.memberSubfamily a) \\to p\\mathcal{A}) \\to \\forall \\mathcal{A}, p\\mathcal{A}$$$
Lean4
/-- Down-compressing a family doesn't change its size. -/
@[simp]
theorem card_compression (a : α) (𝒜 : Finset (Finset α)) : #(𝓓 a 𝒜) = #𝒜 :=
by
rw [compression, card_disjUnion, filter_image, card_image_of_injOn ((erase_injOn' _).mono fun s hs => _), ←
card_union_of_disjoint]
· conv_rhs => rw [← filter_union_filter_neg_eq (fun s => (erase s a ∈ 𝒜)) 𝒜]
· exact disjoint_filter_filter_neg 𝒜 𝒜 (fun s => (erase s a ∈ 𝒜))
intro s hs
rw [mem_coe, mem_filter] at hs
exact not_imp_comm.1 erase_eq_of_notMem (ne_of_mem_of_not_mem hs.1 hs.2).symm
