slice_subset_falling — Mathlib

English

Let 𝒜 be a finite family of subsets of a finite set α. For every natural k, the k-th layer of 𝒜 (the subfamily consisting of those members of 𝒜 of size k) is contained in the k-fold shadow of 𝒜; in symbols, 𝒜_k ⊆ ∂^k 𝒜.

Русский

Пусть 𝒜 — конечное семейство подмножеств множества α. Для любого натурального k слой 𝒜, состоящий из элементов размера k, содержится в k-разовой тени 𝒜; то есть 𝒜_k ⊆ ∂^k 𝒜.

LaTeX

$$$$ 𝒜 \# k \\subseteq \\partial^k 𝒜 $$$$

Lean4

theorem slice_subset_falling : 𝒜 #k ⊆ falling k 𝒜 := fun s hs =>
  mem_falling.2 <| (mem_slice.1 hs).imp_left fun h => ⟨s, h, Subset.refl _⟩

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