type_eq_one_of_unique

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Ordinal.type_eq_one_of_unique

← MathLib Explorer

English

type r = 1 for a well-order with a unique element.

Русский

type r = 1 при наличии уникального элемента в упорядочении.

LaTeX

$$$\mathrm{type}(r) = 1$$$

Lean4

theorem type_eq_one_of_unique (r) [IsWellOrder α r] [Nonempty α] [Subsingleton α] : type r = 1 :=
  by
  cases nonempty_unique α
  exact (RelIso.ofUniqueOfIrrefl r _).ordinal_type_eq

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

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

Разделы

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

Аффилиация

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