inter_cylinder — Mathlib

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

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