smul_inter_subset

Mathlib.Algebra.Group.Pointwise.Set.Scalar

URI: https://scilib.ai/kg/mathlib#Set.smul_inter_subset

English

The product distributes over intersection on the right: 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₂ :=
  image2_inter_subset_right

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru