inter_smul_subset — Mathlib

English

The intersection of s1 and s2, scaled by t, is contained in the intersection of the scaled sets: (s1 ∩ s2) • t ⊆ (s1 • t) ∩ (s2 • t).

Русский

Пересечение s1 и s2, умноженное скаляром t, содержится в пересечении их умножений: (s1 ∩ s2) • t ⊆ (s1 • t) ∩ (s2 • t).

LaTeX

$$$ (s_1 \cap s_2) \cdot t \subseteq (s_1 \cdot t) \cap (s_2 \cdot t) $$$

Lean4

@[to_additive]
theorem inter_smul_subset [DecidableEq α] : (s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t :=
  image₂_inter_subset_left

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