toFinset_card_of_nodup

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#List.toFinset_card_of_nodup

English

If l is Nodup, then #l.toFinset = length(l).

Русский

Если список l без повторов, то #l.toFinset = длина(l).

LaTeX

$$Nodup(l) \Rightarrow #l.toFinset = \operatorname{length}(l)$$

Lean4

theorem toFinset_card_of_nodup {l : List α} (h : l.Nodup) : #l.toFinset = l.length :=
  Multiset.toFinset_card_of_nodup h

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

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

Разделы

Аффилиация

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