card_ne_zero

Mathlib.Data.FinEnum

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

English

No nonempty FinEnum α has card α = 0.

Русский

У непустого FinEnum α не может быть card α = 0.

LaTeX

$$$ \\operatorname{card}(\\\\alpha) \\neq 0. $$$

Lean4

/-- No non-empty enumeration has 0 elements. -/
theorem card_ne_zero {α : Type*} [FinEnum α] [Nonempty α] : card α ≠ 0 :=
  card_pos.ne'

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

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

Разделы

Аффилиация

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