toFinset_card_le

Mathlib.Data.Finset.Card

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

English

The cardinality of m.toFinset is at most the cardinality of m.

Русский

Кардинал m.toFinset не превосходит кардинал m.

LaTeX

$$$#m.toFinset \le #m$$$

Lean4

theorem toFinset_card_le : #m.toFinset ≤ Multiset.card m :=
  card_le_card <| dedup_le _

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

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

Разделы

Аффилиация

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