card_pos

Mathlib.Data.Fintype.Card

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

English

If α is nonempty, then 0 < card α.

Русский

Если α непусто, то 0 < card α.

LaTeX

$$Nonempty(\alpha) \Rightarrow 0 < |\alpha|$$

Lean4

theorem card_pos [h : Nonempty α] : 0 < card α :=
  card_pos_iff.mpr h

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

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

Разделы

Аффилиация

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