card_val

Mathlib.Data.Finset.Card

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

English

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

Русский

Кардинал Multiset s.1 равен кардинальности Finset s: Multiset.card s.1 = #s.

LaTeX

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

Lean4

@[simp]
theorem card_val (s : Finset α) : Multiset.card s.1 = #s :=
  rfl

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

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

Разделы

Аффилиация

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