ext'

Mathlib.Data.Multiset.Count

URI: https://scilib.ai/kg/mathlib#Multiset.ext'

English

If two multisets have the same counts for every element, then they are equal.

Русский

Если два мультимножества имеют одинаковые кратности для каждого элемента, то они равны.

LaTeX

$$(\forall a, \operatorname{count}(a, s) = \operatorname{count}(a, t)) \Rightarrow s = t$$

Lean4

@[ext]
theorem ext' {s t : Multiset α} : (∀ a, count a s = count a t) → s = t :=
  ext.2

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

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

Разделы

Аффилиация

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