cmpLE_eq_cmp — Mathlib

English

In a total preorder with decidable order, the two comparison notions cmpLE and cmp coincide.

Русский

В полном преддорепорядке с решаемостью порядка совпадают понятия сравнения cmpLE и cmp.

LaTeX

$$$cmpLE x y = cmp x y$$$

Lean4

theorem cmpLE_eq_cmp {α} [Preorder α] [IsTotal α (· ≤ ·)] [DecidableLE α] [DecidableLT α] (x y : α) :
    cmpLE x y = cmp x y :=
  by
  by_cases xy : x ≤ y <;> by_cases yx : y ≤ x <;> simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]
  cases not_or_intro xy yx (total_of _ _ _)

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