English
Two cylinders are disjoint if and only if their restricted base sets are disjoint.
Русский
Два цилиндра непересекаются тогда и только тогда, когда их ограниченные основания непересекаются.
LaTeX
$$$ \\mathrm{Disjoint}(\\mathrm{cylinder}(s,S), \\mathrm{cylinder}(t,T)) \\iff \\mathrm{Disjoint}(\\mathrm{Finset.restrict_{2}}(\\subseteq_{\\mathrm{left}})^{-1} S, \\mathrm{Finset.restrict_{2}}(\\subseteq_{\\mathrm{right}})^{-1} T). $$$
Lean4
theorem disjoint_cylinder_iff [Nonempty (∀ i, α i)] {s t : Finset ι} {S : Set (∀ i : s, α i)} {T : Set (∀ i : t, α i)}
[DecidableEq ι] :
Disjoint (cylinder s S) (cylinder t T) ↔
Disjoint (Finset.restrict₂ Finset.subset_union_left ⁻¹' S) (Finset.restrict₂ Finset.subset_union_right ⁻¹' T) :=
by simp_rw [Set.disjoint_iff, subset_empty_iff, inter_cylinder, cylinder_eq_empty_iff]
