isStrictOrderConnected_of_isStrictTotalOrder

English

If a relation is a strict total order, then it is order-connected.

Русский

Если отношение является строгим тотальным порядком, то оно связано относительно порядка.

LaTeX

$$$[IsStrictTotalOrder \\alpha \\ r] \\Rightarrow [IsOrderConnected \\alpha \\ r]$$$

Lean4

instance (priority := 100) isStrictOrderConnected_of_isStrictTotalOrder [IsStrictTotalOrder α r] :
    IsOrderConnected α r :=
  ⟨fun _ _ _ h ↦ (trichotomous _ _).imp_right fun o ↦ o.elim (fun e ↦ e ▸ h) fun h' ↦ _root_.trans h' h⟩

Похожие утверждения