diff_cylinder_same — Mathlib

English

For a finite index set s and two cylinder bases S and T, the set-difference of cylinders equals cylinder of the difference S \\ T.

Русский

Для конечного множества индексов s и оснований цилиндров S и T верно: цилиндр s S минус цилиндр s T равен цилиндру s (S \\ T).

LaTeX

$$$ \\mathrm{cylinder}(s,S) \\setminus \\mathrm{cylinder}(s,T) = \\mathrm{cylinder}(s, S \\setminus T) $$$

Lean4

theorem diff_cylinder_same (s : Finset ι) (S T : Set (∀ i : s, α i)) :
    cylinder s S \ cylinder s T = cylinder s (S \ T) := by ext1 f; simp only [mem_diff, mem_cylinder]

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