union_cylinder_same — Mathlib

English

Union of two cylinders with the same index set equals the cylinder over the same index set with the union of the bases.

Русский

Объединение двух цилиндров с одинаковым набором индексов дает цилиндр над тем же набором индексов с основанием в виде объединения двух оснований.

LaTeX

$$$$\\mathrm{cylinder}(s,S_1) \\cup \\mathrm{cylinder}(s,S_2) = \\mathrm{cylinder}(s,S_1 \\cup S_2).$$$$

Lean4

theorem union_cylinder_same (s : Finset ι) (S₁ : Set (∀ i : s, α i)) (S₂ : Set (∀ i : s, α i)) :
    cylinder s S₁ ∪ cylinder s S₂ = cylinder s (S₁ ∪ S₂) :=
  rfl

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