English
Intersection of cylinders corresponds to cylinder over the union of index sets with the corresponding coordinate-wise intersections of the bases.
Русский
Пересечение цилиндров соответствует цилиндру над объединением наборов индексов и поперечных пересечений оснований.
LaTeX
$$$$\\mathrm{cylinder}(s_1,S_1) \\cap \\mathrm{cylinder}(s_2,S_2) = \\mathrm{cylinder}(s_1 \\cup s_2)\\Big( \\mathrm{restrict₂}\\,S_1 \\cap \\mathrm{restrict₂}\\,S_2 \\Big).$$$$
Lean4
theorem inter_cylinder (s₁ s₂ : Finset ι) (S₁ : Set (∀ i : s₁, α i)) (S₂ : Set (∀ i : s₂, α i)) [DecidableEq ι] :
cylinder s₁ S₁ ∩ cylinder s₂ S₂ =
cylinder (s₁ ∪ s₂)
(Finset.restrict₂ Finset.subset_union_left ⁻¹' S₁ ∩ Finset.restrict₂ Finset.subset_union_right ⁻¹' S₂) :=
rfl