inter_mul_union_subset_union — Mathlib

English

The product with an intersection on the left and a union on the right is contained in the union of products: (s1 ∩ s2) * (t1 ∪ t2) ⊆ (s1 * t1) ∪ (s2 * t2).

Русский

Произведение с пересечением слева и объединением справа содержится в объединении произведений: (s1 ∩ s2) * (t1 ∪ t2) ⊆ (s1 * t1) ∪ (s2 * t2).

LaTeX

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

Lean4

@[to_additive]
theorem inter_mul_union_subset_union : s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂ :=
  image₂_inter_union_subset_union

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