toFinset_union

Mathlib.Data.Finset.Basic

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

English

The Finset corresponding to the union of two multisets equals the union of their Finsets.

Русский

Соответствующее Finset к объединению двух мультисетов равно объединению их Finset-частей.

LaTeX

$$$(s \\cup t).toFinset = s.toFinset \\cup t.toFinset$$$

Lean4

@[simp]
theorem toFinset_union (s t : Multiset α) : (s ∪ t).toFinset = s.toFinset ∪ t.toFinset := by ext; simp

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

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

Разделы

Аффилиация

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