mul_iInter₂_subset — Mathlib

English

For a fixed s and a family t i j, the product s * ⋂ (i) (j), t i j is contained in ⋂ (i) (j), s * t i j.

Русский

Для фиксированного s и семейства t i j, s * ⋂ (i),(j) t i j ⊆ ⋂ (i),(j), s * t i j.

LaTeX

$$$(s * \\bigcap_i (\\bigcap_j t_{i j})) \\subseteq \\bigcap_i (\\bigcap_j (s * t_{i j}))$$$

Lean4

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

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