English
The k-th shadow of 𝒜 is the collection of all sets obtained by removing k elements from members of 𝒜; there is a precise equivalence with the k-th iterate of the shadow operator.
Русский
k-я тень 𝒜 — множество всех множеств, полученных вычитанием k элементов из элементов 𝒜; существует точное соответствие с k-разовым повторением операции тени.
LaTeX
$$$$ t \\in ∂^{[k]} 𝒜 \\iff \\exists s \\in 𝒜, |s \\setminus t| = k $$$$
Lean4
theorem mem_shadow_iterate_iff_exists_card : t ∈ ∂ ^[k] 𝒜 ↔ ∃ u : Finset α, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜 := by
induction k generalizing t with
| zero => simp
| succ k ih =>
simp only [mem_shadow_iff_insert_mem, ih, Function.iterate_succ_apply', card_eq_succ]
aesop