cardEqZeroEquivEquivEmpty

Mathlib.Data.Fintype.Card

URI: https://scilib.ai/kg/mathlib#Fintype.cardEqZeroEquivEquivEmpty

← MathLib Explorer

English

For finite α, card α = 0 is equivalent to α ≃ Empty.

Русский

Для конечного α условие card α = 0 эквивалентно α ≃ Empty.

LaTeX

$$$|\alpha| = 0 \iff (\alpha \simeq Empty)$$$

Lean4

/-- A `Fintype` with cardinality zero is equivalent to `Empty`. -/
def cardEqZeroEquivEquivEmpty : card α = 0 ≃ (α ≃ Empty) :=
  (Equiv.ofIff card_eq_zero_iff).trans (Equiv.equivEmptyEquiv α).symm

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

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

Разделы

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

Аффилиация

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