English
Transfer a preorder from β to α via a function f: α → β: define a ≤ b iff f(a) ≤ f(b) and a < b iff f(a) < f(b).
Русский
Перенос предпорядка с β на α через функцию f: α → β: определить a ≤ b, если f(a) ≤ f(b), и a < b, если f(a) < f(b).
LaTeX
$$$\text{lift}(f) : \text{Preorder}(\alpha) \\ a \le b \iff f(a) \le f(b),\quad a < b \iff f(a) < f(b)$$$
Lean4
/-- Transfer a `Preorder` on `β` to a `Preorder` on `α` using a function `f : α → β`.
See also `Function.Injective.preorder` when only the proof fields need to be transferred.
See note [reducible non-instances]. -/
abbrev lift [Preorder β] (f : α → β) : Preorder α :=
letI _instLE : LE α := ⟨fun a b ↦ f a ≤ f b⟩
letI _instLT : LT α := ⟨fun a b ↦ f a < f b⟩
Function.Injective.preorder f .rfl .rfl
