card_empty

Mathlib.Data.Finset.Card

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

English

The Finset of the empty set has cardinality zero: #(∅) = 0.

Русский

Финсет пустого множества имеет кардинал равный нулю: #(∅) = 0.

LaTeX

$$$\#(\emptyset) = 0$$$

Lean4

@[simp, grind =]
theorem card_empty : #(∅ : Finset α) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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