finite_toSet_toFinset

Mathlib.Data.Set.Finite.Basic

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

English

For a multiset s with decidable equality, the toFinset of finite_toSet equals toFinset of s.

Русский

Для мультсета s сDecidableEq верно toFinset(finite_toSet(s)) = s.toFinset.

LaTeX

$$$\\text{toFinset}(\\operatorname{finite\\_toSet}(s)) = s.toFinset.$$$

Lean4

@[simp]
theorem finite_toSet_toFinset [DecidableEq α] (s : Multiset α) : s.finite_toSet.toFinset = s.toFinset :=
  by
  ext x
  simp

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

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

Разделы

Аффилиация

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