toDFinsupp_union

Mathlib.Data.DFinsupp.Multiset

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

English

toDFinsupp(s ∪ t) equals toDFinsupp s ⊔ toDFinsupp t.

Русский

toDFinsupp(s ∪ t) равно toDFinsupp s ⊔ toDFinsupp t.

LaTeX

$$$$ \\operatorname{toDFinsupp}(s \\cup t) = \\operatorname{toDFinsupp}(s) \\sqcup \\operatorname{toDFinsupp}(t) $$$$

Lean4

@[simp]
theorem toDFinsupp_union (s t : Multiset α) : toDFinsupp (s ∪ t) = toDFinsupp s ⊔ toDFinsupp t := by ext i; simp

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

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

Разделы

Аффилиация

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