card

Mathlib.Order.Atoms.Finite

URI: https://scilib.ai/kg/mathlib#Fintype.IsSimpleOrder.card

English

For a finite simple order α with decidable equality, the cardinality is 2.

Русский

Для конечного простого порядка α с разрешимой эквивалентностью кардинальность равна двум.

LaTeX

$$$\\#\\alpha = 2$$$

Lean4

theorem card : Fintype.card α = 2 :=
  (Fintype.ofEquiv_card _).trans Fintype.card_bool

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

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

Разделы

Аффилиация

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