iInter_smul_subset — Mathlib

English

The intersection of indexed sets, smul by t, is a subset of the intersection of each smul: (⋂ i, s i) • t ⊆ ⋂ i, s i • t.

Русский

Пересечение семейства множеств, умноженное на t, содержится в пересечении всех smul: (⋂ i, s i) • t ⊆ ⋂ i, s i • t.

LaTeX

$$$$ \left( \bigcap_i s_i \right) \cdot t \subseteq \bigcap_i (s_i \cdot t) $$$$

Lean4

@[to_additive]
theorem iInter_smul_subset (s : ι → Set α) (t : Set β) : (⋂ i, s i) • t ⊆ ⋂ i, s i • t :=
  image2_iInter_subset_left ..

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