slice — Mathlib

English

For a family 𝒜 of Finset α and a natural r, the r-th slice consists of those A in 𝒜 with |A| = r.

Русский

Для семейства 𝒜 подмножеств α и нат. числа r срез с размером r состоит из таких A ∈ 𝒜, что |A| = r.

LaTeX

$$$ (𝒜 : Finset (Finset α))\ # r = \{ A ∈ 𝒜 \mid |A| = r \}$$$

Lean4

/-- The `r`-th slice of a set family is the subset of its elements which have cardinality `r`. -/
def slice (𝒜 : Finset (Finset α)) (r : ℕ) : Finset (Finset α) :=
  {A ∈ 𝒜 | #A = r}

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