smul_iInter_subset — Mathlib

English

The smul of a set by an intersection is contained in the intersection of smul by each factor: (s • ⋂ i, t i) ⊆ ⋂ i, s • t i.

Русский

Умножение множества s на пересечение ограничено пересечением smul по каждому t i: (s • ⋂ i, t i) ⊆ ⋂ i, s • t i.

LaTeX

$$$$ (s \cdot \bigcap_i t_i) \subseteq \bigcap_i (s \cdot t_i) $$$$

Lean4

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

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