English
If o and a,b satisfy Compares o a b, then o = lt if and only if a < b.
Русский
Если o сравнивает a и b и выполняется Compares o a b, то o = lt тогда и только тогда, когда a < b.
LaTeX
$$$\\forall o\\ {a b},\\ Compares o a b \\rightarrow (o = \{lt\} \\leftrightarrow a < b)$$$
Lean4
theorem eq_lt [Preorder α] : ∀ {o} {a b : α}, Compares o a b → (o = lt ↔ a < b)
| lt, _, _, h => ⟨fun _ => h, fun _ => rfl⟩
| eq, a, b, h => ⟨fun h => by injection h, fun h' => (ne_of_lt h' h).elim⟩
| gt, a, b, h => ⟨fun h => by injection h, fun h' => (lt_asymm h h').elim⟩