union_smul_inter_subset_union — Mathlib

English

Let s1, s2 ⊆ A and t1, t2 ⊆ B with a scalar action. Then (s1 ∪ s2) · (t1 ∩ t2) ⊆ s1 · t1 ∪ s2 · t2.

Русский

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

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