∀ {ι : Type u_1} (X : ι → Type u_2) [inst : (i : ι) → TopologicalSpace (X i)],
  MeasureTheory.closedCompactCylinders X =
    ⋃ s, ⋃ S, ⋃ (_ : IsClosed S), ⋃ (_ : IsCompact S), {MeasureTheory.cylinder s S}