inter_mul_subset

Mathlib.Algebra.Group.Pointwise.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.inter_mul_subset

English

The product distributes over intersection in one side: (s1 ∩ s2) * t is contained in (s1 * t) ∩ (s2 * t).

Русский

Произведение распределяется по пересечению слева: (s1 ∩ s2) * t ⊆ (s1 * t) ∩ (s2 * t).

LaTeX

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

Lean4

@[to_additive]
theorem inter_mul_subset : s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t) :=
  image₂_inter_subset_left

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

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

Разделы

Аффилиация

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