inter_smul_subset

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

The product distributes over intersection on the left: (s1 ∩ s2) • t ⊆ s1 • t ∩ 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 : (s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t :=
  image2_inter_subset_left

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

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

Разделы

Аффилиация

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