union_smul_inter_subset_union — Mathlib

English

The union-interaction of a union and an intersection is contained in the union of the corresponding products: (s1 ∪ s2) • (t1 ∩ t2) ⊆ (s1 • t1) ∪ (s2 • t2).

Русский

Объединение и пересечение в сочетании с умножением содержатся в объединении соответствующих произведений: (s1 ∪ s2) • (t1 ∩ t2) ⊆ (s1 • t1) ∪ (s2 • t2).

LaTeX

$$$ (s_1 \cup s_2) \cdot (t_1 \cap t_2) \subseteq (s_1 \cdot t_1) \cup (s_2 \cdot t_2) $$$

Lean4

@[to_additive]
theorem union_smul_inter_subset_union [DecidableEq α] : (s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂ :=
  image₂_union_inter_subset_union

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