inter_cylinder_same — Mathlib

English

If the two cylinders share the same index set, their intersection equals the cylinder of the intersection of the bases.

Русский

Если цилиндры имеют общий набор индексов, их пересечение равно цилиндру над пересечением оснований.

LaTeX

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

Lean4

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

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