English
Square cylinders consist of products of a finite subset of indices with a product of sets in each coordinate, such that each coordinate is chosen from a given family C(i).
Русский
Квадратные цилиндры состоят из произведений по конечному подмножеству индексов и произведений множеств по каждой координате, где для каждой координаты выбирается множество из семейства C(i).
LaTeX
$$$$\\text{squareCylinders}(C) = \\{ S : \\text{Set}((i:\\iota)\\to \\alpha_i) \\mid ∃ s:\\text{Finset }\\iota, ∃ t ∈ univ.pi C, S = (s: \\text{Set }\\iota).pi t \\}.$$$$
Lean4
/-- Given a finite set `s` of indices, a square cylinder is the product of a set `S` of
`∀ i : s, α i` and of `univ` on the other indices. The set `S` is a product of sets `t i` such that
for all `i : s`, `t i ∈ C i`.
`squareCylinders` is the set of all such squareCylinders. -/
def squareCylinders (C : ∀ i, Set (Set (α i))) : Set (Set (∀ i, α i)) :=
{S | ∃ s : Finset ι, ∃ t ∈ univ.pi C, S = (s : Set ι).pi t}
