English
Let 𝒜 be a finite family of finite subsets of a ground set α and let a be an element of α. The operation that retains only those members of 𝒜 that do not contain a, when applied twice with the same a, yields the same subfamily as applying it once: (𝒜.nonMemberSubfamily a).nonMemberSubfamily a = 𝒜.nonMemberSubfamily a.
Русский
Пусть 𝒜 — конечное семейство конечных подмножеств множества α, и пусть a — элемент α. Операция выделения подсемейства без a, применяемая дважды к одному и тому же a, дает то же самое подсемейство, что и один раз: (𝒜.nonMemberSubfamily a).nonMemberSubfamily a = 𝒜.nonMemberSubfamily a.
LaTeX
$$$ (\\mathcal{A}_{a}^{-})_{a}^{-} = \\mathcal{A}_{a}^{-} \\quad\\text{where } \\mathcal{A}_{a}^{-} := \\{ S \\in \\mathcal{A} \\mid a \\notin S \\}. $$$
Lean4
@[simp]
theorem nonMemberSubfamily_nonMemberSubfamily :
(𝒜.nonMemberSubfamily a).nonMemberSubfamily a = 𝒜.nonMemberSubfamily a :=
by
ext
simp
