disjSum_zero

Mathlib.Data.Multiset.Sum

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

English

The disjoint sum with the zero multiset on the right is obtained by mapping the left multiset with inl.

Русский

Дизъюнкционное сложение слева с нулевым мультсетoм справа даёт s.map inl.

LaTeX

$$$$ s.\\operatorname{disjSum} (0 : \\operatorname{Multiset} \\beta) = s.map inl $$$$

Lean4

@[simp]
theorem disjSum_zero : s.disjSum (0 : Multiset β) = s.map inl :=
  Multiset.add_zero _

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

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

Разделы

Аффилиация

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