instTransOrd_mathlib

Mathlib.Order.ULift

URI: https://scilib.ai/kg/mathlib#ULift.instTransOrd_mathlib

English

If α has an order, ULift α inherits a TransOrd structure with isLE_trans carried over from α.

Русский

Если у α есть порядок, ULift α наследует структуру TransOrd и свойство isLE_trans переносится с α.

LaTeX

$$$isLE\\_trans^{ULift} = isLE\\_trans^{α}$$$

Lean4

instance [Ord α] [inst : Std.TransOrd α] : Std.TransOrd (ULift.{v} α) where isLE_trans := inst.isLE_trans

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

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

Разделы

Аффилиация

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