cylinder_mem_closedCompactCylinders

English

The intersection of two cylinders with possibly different index sets is another cylinder over the union of the index sets with the corresponding restricted bases.

Русский

Пересечение двух цилиндров с различными наборами индексов равно цилиндру над объединением наборов индексов с соответствующими ограничениями оснований.

LaTeX

$$$$\\mathrm{cylinder}(s_1,S_1) \\cap \\mathrm{cylinder}(s_2,S_2) = \\mathrm{cylinder}(s_1 \\cup s_2)(\\mathrm{restrict₂}\\,S_1 \\cap \\mathrm{restrict₂}\\,S_2).$$$$

Lean4

theorem cylinder_mem_closedCompactCylinders (s : Finset ι) (S : Set (Π i : s, X i)) (hS_closed : IsClosed S)
    (hS_compact : IsCompact S) : cylinder s S ∈ closedCompactCylinders X :=
  by
  rw [mem_closedCompactCylinders]
  exact ⟨s, S, hS_closed, hS_compact, rfl⟩

Похожие утверждения