card_def

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#Finset.card_def

English

The cardinality of a Finset s equals the cardinality of its underlying Multiset representation: #s = Multiset.card s.1.

Русский

Кардинальность Finset s равна кардинальности его базовой мультисеты: #s = Multiset.card s.1.

LaTeX

$$$#s = \operatorname{Multiset.card} \; s.1$$$

Lean4

theorem card_def (s : Finset α) : #s = Multiset.card s.1 :=
  rfl

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

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

Разделы

Аффилиация

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