zero_union

Mathlib.Data.Multiset.UnionInter

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

English

The union with the zero multiset leaves the other multiset unchanged: 0 ∪ s = s.

Русский

Объединение с нулём не изменяет множества: 0 ∪ s = s.

LaTeX

$$$0 \\cup s = s$$$

Lean4

@[simp]
theorem zero_union : 0 ∪ s = s := by simp [union_def, Multiset.zero_sub]

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

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

Разделы

Аффилиация

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