shadow_iterate — Mathlib

English

The k-th shadow of a family 𝒜 is a family of r−k-sets; more precisely, Set.Sized r 𝒜.toSet → Set.Sized (r−k) (∂^[k] 𝒜).

Русский

k-я тень семейства 𝒜 есть семейство множеств размера r−k; точнее, If 𝒜 размеры r, то ∂^[k] 𝒜 имеет размер r−k.

LaTeX

$$$$ \\text{Set.Sized}_{r-k}(∂^{[k]} 𝒜) $$$$

Lean4

/-- The `k`-th shadow of a family of `r`-sets is a family of `r - k`-sets. -/
theorem _root_.Set.Sized.shadow_iterate (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
    (∂ ^[k] 𝒜 : Set (Finset α)).Sized (r - k) :=
  by
  simp_rw [Set.Sized, mem_coe, mem_shadow_iterate_iff_exists_sdiff]
  rintro t ⟨s, hs, hts, rfl⟩
  rw [card_sdiff_of_subset hts, ← h𝒜 hs, Nat.sub_sub_self (card_le_card hts)]

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