instLawfulLEOrd_mathlib

Mathlib.Order.ULift

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

English

If α has LE and Ord and LawfulLEOrd, ULift α inherits LawfulLEOrd.

Русский

Если у α есть LE и Ord и LawfulLEOrd, ULift α наследует LawfulLEOrd.

LaTeX

$$$[LE\\;α] \\land [Ord\\;α] \\land [LawfulLEOrd\\;α] \\Rightarrow [LawfulLEOrd\\;ULift\\;α]$$$

Lean4

instance [LE α] [Ord α] [inst : Std.LawfulLEOrd α] : Std.LawfulLEOrd (ULift.{v} α) where isLE_iff_le := inst.isLE_iff_le

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

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

Разделы

Аффилиация

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