English
If a and b are in a linear order and a', b' in a preorder, and for all o, Compares o a b implies Compares o a' b', then for every o, Compares o a b iff Compares o a' b'.
Русский
Если для линейного порядка a и b в целостном порядке и для любых o выполняется: Compares o a b → Compares o a' b', тогда для каждого o выполняется: Compares o a b ↔ Compares o a' b'.
LaTeX
$$$[LinearOrder\,\alpha] [Preorder\,\beta] \{a b : \alpha\} \{a' b' : \beta\} (h : \forall o, Compares o a b \rightarrow Compares o a' b') \ (o) : Compares o a b \leftrightarrow Compares o a' b'$$$
Lean4
theorem compares_iff_of_compares_impl [LinearOrder α] [Preorder β] {a b : α} {a' b' : β}
(h : ∀ {o}, Compares o a b → Compares o a' b') (o) : Compares o a b ↔ Compares o a' b' :=
by
refine ⟨h, fun ho => ?_⟩
rcases lt_trichotomy a b with hab | hab | hab
· have hab : Compares Ordering.lt a b := hab
rwa [ho.inj (h hab)]
· have hab : Compares Ordering.eq a b := hab
rwa [ho.inj (h hab)]
· have hab : Compares Ordering.gt a b := hab
rwa [ho.inj (h hab)]
