union_mul_inter_subset

Mathlib.Algebra.Group.Pointwise.Set.Basic

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

English

In a commutative semigroup, (s ∪ t) * (s ∩ t) ⊆ s * t.

Русский

В коммутативной полугруппе выполняется: (s ∪ t) * (s ∩ t) ⊆ s * t.

LaTeX

$$$$ (s \cup t) * (s \cap t) \subseteq s * t. $$$$

Lean4

@[to_additive]
theorem union_mul_inter_subset : (s ∪ t) * (s ∩ t) ⊆ s * t :=
  image2_union_inter_subset mul_comm

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

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

Разделы

Аффилиация

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