isStrictWeakOrder_of_isOrderConnected

English

If a relation on a type is antisymmetric and order-connected, then it is a strict weak order.

Русский

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

LaTeX

$$$\\forall {\\alpha} {r[:]} [IsAsymm \\alpha \\ r] [IsOrderConnected \\alpha \\ r], IsStrictWeakOrder \\alpha \\ r$$

Lean4

theorem isStrictWeakOrder_of_isOrderConnected [IsAsymm α r] [IsOrderConnected α r] : IsStrictWeakOrder α r :=
  { @IsAsymm.isIrrefl α r _ with trans := fun _ _ c h₁ h₂ => (IsOrderConnected.conn _ c _ h₁).resolve_right (asymm h₂),
    incomp_trans := fun _ _ _ ⟨h₁, h₂⟩ ⟨h₃, h₄⟩ =>
      ⟨IsOrderConnected.neg_trans h₁ h₃, IsOrderConnected.neg_trans h₄ h₂⟩ }
    -- see Note [lower instance priority]

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