English
The upper shadow of a family 𝒜 is all sets obtained by adding one element to any member of 𝒜; the k-fold iterated upper shadow adds k elements from members of 𝒜.
Русский
Верхняя тень семейства 𝒜 состоит из всех множеств, которые можно получить, добавив к любому элементу 𝒜 ещё по одному элементу; k-кратная итерация добавляет k элементов.
LaTeX
$$$ upShadow(𝒜) \;:\; Finset( Finset(α) )\to Finset( Finset(α) ) \\text{ и }\; upShadow^{[k]}(𝒜) \text{ состоит из наборов, получаемых добавлением } k \text{ элементов.}$$$
Lean4
/-- The upper shadow of a set family `𝒜` is all sets we can get by adding one element to any set in
`𝒜`, and the (`k` times) iterated upper shadow (`upShadow^[k]`) is all sets we can get by adding
`k` elements from any set in `𝒜`. -/
def upShadow (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
𝒜.sup fun s => sᶜ.image fun a => insert a s
