lift

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#PartialOrder.lift

Lean4

/-- Transfer a `PartialOrder` on `β` to a `PartialOrder` on `α` using an injective
function `f : α → β`.

See also `Function.Injective.partialOrder` when only the proof fields need to be transferred.

See note [reducible non-instances]. -/
abbrev lift [PartialOrder β] (f : α → β) (inj : Injective f) : PartialOrder α :=
  letI _instLE : LE α := ⟨fun a b ↦ f a ≤ f b⟩
  letI _instLT : LT α := ⟨fun a b ↦ f a < f b⟩
  Function.Injective.partialOrder f inj .rfl .rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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