card_eq_zero

Mathlib.Data.FinEnum

URI: https://scilib.ai/kg/mathlib#FinEnum.card_eq_zero

← MathLib Explorer

English

If α is empty, then card α = 0.

Русский

Если α пуст, то card α = 0.

LaTeX

$$$ \\text{If } IsEmpty(\\\\alpha)\\text{, then } \\operatorname{card}(\\\\alpha) = 0. $$$

Lean4

/-- Any enumeration of an empty type has length 0. -/
theorem card_eq_zero {α : Type u} [FinEnum α] [IsEmpty α] : card α = 0 :=
  card_eq_zero_iff.mpr ‹_›

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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