sInter_smul_subset — Mathlib

English

The intersection of a family of sets, smul by t, is contained in the intersection over members of the family smul by t: S.sInter t ⊆ ⋂ s ∈ S, s • t.

Русский

Пересечение семейства множеств, умноженное на t, содержится в пересечении каждого smul: S.sInter t ⊆ ⋂ s ∈ S, s • t.

LaTeX

$$$$ \left( S \cap\_{{s \in S}} \; t \right) \subseteq \bigcap_{s \in S} (s \cdot t) $$$$

Lean4

@[to_additive]
theorem sInter_smul_subset (S : Set (Set α)) (t : Set β) : ⋂₀ S • t ⊆ ⋂ s ∈ S, s • t :=
  image2_sInter_left_subset S t (fun a x => a • x)

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