shadow — Mathlib

English

The shadow ∂ 𝒜 of a set family 𝒜 is the family of all sets obtained by removing one element from any member of 𝒜.

Русский

Тень ∂ 𝒜 множества — это семейство всех множеств, полученных вычитанием одного элемента из любого элемента 𝒜.

LaTeX

$$$$ \\partial 𝒜 = \\{ s \\setminus \\{a\\} : s \\in 𝒜, a \\in s \\} $$$$

Lean4

/-- The shadow of a set family `𝒜` is all sets we can get by removing one element from any set in
`𝒜`, and the (`k` times) iterated shadow (`shadow^[k]`) is all sets we can get by removing `k`
elements from any set in `𝒜`. -/
def shadow (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
  𝒜.sup fun s => s.image (erase s)

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