isWellOrder_lt

Mathlib.Order.Extension.Well

URI: https://scilib.ai/kg/mathlib#IsWellFounded.wellOrderExtension.isWellOrder_lt

English

Szpilrajn extension theorem: any partial order can be extended to a linear order.

Русский

Теорема о разширении Szpilrajn: любой частичный порядок можно расширить до линейного порядка.

LaTeX

$$$\exists s : α → α → Prop, IsLinearOrder α s ∧ r ≤ s$$$

Lean4

instance isWellOrder_lt : IsWellOrder α (wellOrderExtension r).lt where

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

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

Разделы

Аффилиация

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