inter_smul_union_subset_union — Mathlib

English

The product of an intersection with a union 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 \cap s_2) \cdot (t_1 \cup t_2) \subseteq (s_1 \cdot t_1) \cup (s_2 \cdot t_2) $$$

Lean4

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

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