instLawfulBEqOrd_mathlib

Mathlib.Order.ULift

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

English

Given BEq α, Ord α, and LawfulBEq α, ULift α inherits LawfulBEqOrd.

Русский

При наличии BEq α, Ord α и LawfulBEq α ULift α наследует LawfulBEqOrd.

LaTeX

$$$[BEq\\;α] \\land [Ord\\;α] \\land [LawfulBEq\\;α] \\Rightarrow [LawfulBEqOrd\\;ULift\\;α]$$$

Lean4

instance [BEq α] [Ord α] [inst : Std.LawfulBEqOrd α] : Std.LawfulBEqOrd (ULift.{v} α) where
  compare_eq_iff_beq := inst.compare_eq_iff_beq

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

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

Разделы

Аффилиация

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