mem_shadow_iterate_iff_exists_card

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

Похожие утверждения