inter_smul_union_subset_union — Mathlib

English

Let s1, s2 be subsets of a set A and t1, t2 be subsets of a set B, with a scalar action of A on B. Then every element of (s1 ∩ s2) · (t1 ∪ t2) is contained in (s1 · t1) ∪ (s2 · t2); i.e., (s1 ∩ s2) · (t1 ∪ t2) ⊆ s1 · t1 ∪ s2 · t2.

Русский

Пусть s1, s2 — подмножества множества A, t1, t2 — подмножества множества B, и скалярное действие A на B задано. Тогда каждый элемент (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 : (s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂ :=
  image2_inter_union_subset_union

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