English
A linear order structure can be built on a Succ-Archimedean type, provided directedness and decidability assumptions.
Русский
Для типа с SuccArchimedean можно построить линейный порядок при условии направленности и разрешимости.
LaTeX
$$$\text{IsSuccArchimedean}(\text{linearOrder}(\alpha))$$$
Lean4
/-- This isn't an instance due to a loop with `LinearOrder`.
-/
-- See note [reducible non-instances]
abbrev linearOrder [SuccOrder α] [IsSuccArchimedean α] [DecidableEq α] [DecidableLE α] [DecidableLT α]
[IsDirected α (· ≥ ·)] : LinearOrder α
where
le_total a
b :=
have ⟨c, ha, hb⟩ := directed_of (· ≥ ·) a b
le_total_of_codirected ha hb
toDecidableEq := inferInstance
toDecidableLE := inferInstance
toDecidableLT := inferInstance
