univ

Mathlib.Order.Atoms.Finite

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

← MathLib Explorer

English

If α is a finite simple order, then Fintype.card α = 2.

Русский

Если α конечен и прост в порядке, то кардинал Fintype α равен 2.

LaTeX

$$$|\\alpha| = 2$$$

Lean4

theorem univ : (Finset.univ : Finset α) = {⊤, ⊥} :=
  by
  change Finset.map _ (Finset.univ : Finset Bool) = _
  rw [Fintype.univ_bool]
  simp only [Finset.map_insert, Function.Embedding.coeFn_mk, Finset.map_singleton]
  rfl

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

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

Разделы

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

Аффилиация

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