English
The collection of cylinders whose base is closed and compact is formed by taking all finite index sets and all closed compact bases and then collecting the corresponding cylinders.
Русский
Сбор цилиндров, основание которых замкнутое и компактное, образован путём рассмотрения всех конечных наборов индексов и всех замкнутых компактных оснований, а затем соответствующих цилиндров.
LaTeX
$$$$\\text{closedCompactCylinders}(X) = \\bigcup_{s \\in \\mathrm{Finset}(\\iota)} \\bigcup_{S \\subseteq \\prod_{i \\in s} X_i} \\bigl\\{ \\mathrm{cylinder}(s,S) \\ :\\ IsClosed(S) \\wedge IsCompact(S) \\bigr\\}.$$$$
Lean4
/-- The set of all cylinders based on closed compact sets. Note that such a set is closed, but
not compact in general (for instance, the whole space is always a closed compact cylinder). -/
def closedCompactCylinders : Set (Set (Π i, X i)) :=
⋃ (s) (S) (_ : IsClosed S) (_ : IsCompact S), {cylinder s S}
