compl_cylinder — Mathlib

English

Let s be a finite index set and S a subset of the space of functions defined on s. Then the complement of the cylinder cylinder s S equals cylinder s S^c.

Русский

Пусть s — конечное множество индексов, а S — множество функций, определённых на s. Тогда комплемент цилиндра Cyl(s,S) равен Cyl(s,S^c).

LaTeX

$$$ (\\mathrm{cylinder}(s,S))^{c} = \\mathrm{cylinder}(s, S^{c}) $$$

Lean4

theorem compl_cylinder (s : Finset ι) (S : Set (∀ i : s, α i)) : (cylinder s S)ᶜ = cylinder s (Sᶜ) := by ext1 f;
  simp only [mem_compl_iff, mem_cylinder]

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