instIsWellOrderOfIsEmpty

Mathlib.Order.RelClasses

URI: https://scilib.ai/kg/mathlib#instIsWellOrderOfIsEmpty

← MathLib Explorer

English

If α is empty, then for any r, IsWellOrder α r holds.

Русский

Если α пуст, то для любого r выполняется, что α упорядовано по r.

LaTeX

$$IsWellOrder α r$$

Lean4

instance (priority := 100) [IsEmpty α] (r : α → α → Prop) : IsWellOrder α r
    where
  trichotomous := isEmptyElim
  trans := isEmptyElim
  wf := wellFounded_of_isEmpty r

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

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

Разделы

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

Аффилиация

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