singleton_join

Mathlib.Data.Multiset.Bind

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

English

The join of a singleton multiset of a is a.

Русский

Объединение одиночного мультимножества {a} даёт a.

LaTeX

$$$\\operatorname{join}(\\{a\\}) = a$$$

Lean4

@[simp]
theorem singleton_join (a) : join ({ a } : Multiset (Multiset α)) = a :=
  sum_singleton _

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

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

Разделы

Аффилиация

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