zero_disjSum

Mathlib.Data.Multiset.Sum

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

English

The disjoint sum of the zero multiset and t is obtained by mapping t with inr.

Русский

Дизъюнкциональное сложение нулевого мультсетa и t получаемо отображением t через inr.

LaTeX

$$$$ (0 : \\operatorname{Multiset} \\alpha).\\operatorname{disjSum} t = t.map \\mathrm{inr} $$$$

Lean4

@[simp]
theorem zero_disjSum : (0 : Multiset α).disjSum t = t.map inr :=
  Multiset.zero_add _

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

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

Разделы

Аффилиация

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