union_cylinder — Mathlib

English

Union of cylinders with possibly different index sets is the cylinder over the union of indices with the union of the corresponding restricted bases.

Русский

Объединение цилиндров с различными наборами индексов равно цилиндру над объединением индексов с объединением ограниченных оснований.

LaTeX

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

Lean4

theorem union_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

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