instLawfulLTOrd_mathlib

Mathlib.Order.ULift

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

English

If α has LT and Ord and LawfulLTOrd, ULift α inherits LawfulLTOrd.

Русский

Если у α есть LT и Ord и LawfulLTOrd, то ULift α наследует LawfulLTOrd.

LaTeX

$$$[LT\\;α] \\land [Ord\\;α] \\land [LawfulLTOrd\\;α] \\Rightarrow [LawfulLTOrd\\;ULift\\;α]$$$

Lean4

instance [LT α] [Ord α] [inst : Std.LawfulLTOrd α] : Std.LawfulLTOrd (ULift.{v} α) where
  eq_lt_iff_lt := inst.eq_lt_iff_lt

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

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

Разделы

Аффилиация

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