smul_inter_subset — Mathlib

English

The scalar product distributes over the intersection in the first factor: s • (t1 ∩ t2) ⊆ (s • t1) ∩ (s • t2).

Русский

Действие скаляра распределяется по пересечению в первой компоненте: s • (t1 ∩ t2) ⊆ (s • t1) ∩ (s • t2).

LaTeX

$$$ s \cdot (t_1 \cap t_2) \subseteq (s \cdot t_1) \cap (s \cdot t_2) $$$

Lean4

@[to_additive]
theorem smul_inter_subset : s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂ :=
  image₂_inter_subset_right

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