iInter₂_mul_subset — Mathlib

English

For a family s i j, the double intersection multiplied by t is contained in the double intersection of the products: (⋂ i (⋂ j), s i j) * t ⊆ ⋂ i (⋂ j), s i j * t.

Русский

Для двойного пересечения s i j умноженного на t содержится в двойном пересечении произведений s i j * t.

LaTeX

$$$(\\bigcap_i (\\bigcap_j s_{i j})) * t \\subseteq \\bigcap_i (\\bigcap_j (s_{i j} * t))$$$

Lean4

@[to_additive]
theorem iInter₂_mul_subset (s : ∀ i, κ i → Set α) (t : Set α) : (⋂ (i) (j), s i j) * t ⊆ ⋂ (i) (j), s i j * t :=
  image2_iInter₂_subset_left ..

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