gt

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.IsWellOrder.gt

English

If α is well-ordered by >, then WithTop α is well-ordered by >.

Русский

Если ≤ α хорошо упорядочено по '>' тогда WithTop α хорошо упорядочено по '>'.

LaTeX

$$$\\operatorname{WellOrder}(\\mathrm{WithTop}\\,\\alpha, >)$ provided $\\operatorname{WellOrder}(\\alpha, >)$.$$

Lean4

instance gt [Preorder α] [IsWellOrder α (· > ·)] : IsWellOrder (WithTop α) (· > ·) where

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

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

Разделы

Аффилиация

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