join_add

Mathlib.Data.Multiset.Bind

URI: https://scilib.ai/kg/mathlib#Multiset.join_add

English

The join of a sum of multisets equals the sum of their joins.

Русский

Объединение суммы мультимножест равно сумме их объединений.

LaTeX

$$$\\operatorname{join}(S + T) = \\operatorname{join}(S) + \\operatorname{join}(T)$$$

Lean4

@[simp]
theorem join_add (S T) : @join α (S + T) = join S + join T :=
  sum_add _ _

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

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

Разделы

Аффилиация

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