English
There is a construction that pulls back a preorder from β to α along an injective f: α → β, using a specification that x ≤ y iff f x ≤ f y and similarly for <.
Русский
Существует конструкция переноса предпорядка по инъекции f: α → β на α, используя определение x ≤ y ⇔ f x ≤ f y и аналогично для <.
LaTeX
$$$\text{Preorder on } α: a \le b \iff f(a) \le f(b),\; a < b \iff f(a) < f(b)$$$
Lean4
/-- Pull back a `Preorder` instance along an injective function.
See note [reducible non-instances]. -/
abbrev preorder [Preorder β] [LE α] [LT α] (f : α → β) (le : ∀ {x y}, f x ≤ f y ↔ x ≤ y)
(lt : ∀ {x y}, f x < f y ↔ x < y) : Preorder α
where
le_refl _ := le.1 <| le_refl _
le_trans _ _ _ h₁ h₂ := le.1 <| le_trans (le.2 h₁) (le.2 h₂)
lt_iff_le_not_ge _ _ := by rw [← le, ← le, ← lt, lt_iff_le_not_ge]
