English
If α is PredOrder with IsPredArchimedean, then there is a LinearOrder structure on α that can be obtained by transporting a linear order from the dual (order opposite) and reconciling directions.
Русский
Если α является PredOrder с IsPredArchimedean, то на α существует структура линейного порядка, получаемая переносом линейного порядка из двойственного порядка и приведением к исходному порядку.
LaTeX
$$$ \text{There exists a linear order on } \alpha \text{ compatible with the pred-order structure, obtained via the dual construction.}$$$
Lean4
/-- This isn't an instance due to a loop with `LinearOrder`.
-/
-- See note [reducible non-instances]
abbrev linearOrder [PredOrder α] [IsPredArchimedean α] [DecidableEq α] [DecidableLE α] [DecidableLT α]
[IsDirected α (· ≤ ·)] : LinearOrder α :=
letI : LinearOrder αᵒᵈ := IsSuccArchimedean.linearOrder
inferInstanceAs (LinearOrder αᵒᵈᵒᵈ)
