English
Let S be a subset of an additive group and let T(i, j) be a family of subsets indexed by i and j. Then the Minkowski-difference of S with the intersection over all i and j of T(i, j) is contained in the intersection, over all i and j, of the Minkowski-differences of S with T(i, j):\nS -ᵥ ⋂i, ⋂j T(i, j) ⊆ ⋂i, ⋂j (S -ᵥ T(i, j)).
Русский
Пусть S ⊆ β и T(i, j) — семейство множеств в β, индексируемое i и j. Тогда разность по векторам S −ᵥ ⋂i ⋂j T(i, j) вложена в пересечение по всем i, j от S −ᵥ T(i, j).
LaTeX
$$$ s -^\\! v \\, \\bigcap_i \\bigcap_j t(i,j) \\subseteq \\bigcap_i \\bigcap_j (s -^\\\\! v \\, t(i,j)) $$$
Lean4
theorem vsub_iInter₂_subset (s : Set β) (t : ∀ i, κ i → Set β) : s -ᵥ ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s -ᵥ t i j :=
image2_iInter₂_subset_right ..
