subtype_nonempty

Mathlib.SetTheory.Cardinal.Order

URI: https://scilib.ai/kg/mathlib#IsWellOrder.subtype_nonempty

English

The set of all r with IsWellOrder α r is inhabited; there exists a nonempty subtype of well-orders on α.

Русский

Существует непустой подтип отношений, делающих α хорошо упорядоченным.

LaTeX

$$$\\exists r\\; (r \\text{ such that } IsWellOrder(\\alpha, r))$$$

Lean4

instance subtype_nonempty : Nonempty { r // IsWellOrder α r } :=
  ⟨⟨WellOrderingRel, inferInstance⟩⟩

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

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

Разделы

Аффилиация

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