compare_ge_iff_ge — Mathlib

English

In a linear order, compare(a,b) ≠ Ordering.lt iff b ≤ a.

Русский

В линейном порядке compare(a,b) ≠ Ordering.lt тогда и только тогда, когда b ≤ a.

LaTeX

$$$\operatorname{compare}(a,b) \neq \mathrm{Ordering.lt} \iff b \le a$$$

Lean4

theorem compare_ge_iff_ge : compare a b ≠ .lt ↔ b ≤ a :=
  by
  cases h : compare a b
  · simpa using compare_lt_iff_lt.1 h
  · simpa using le_of_eq <| (·.symm) <| compare_eq_iff_eq.1 h
  · simpa using le_of_lt <| compare_gt_iff_gt.1 h

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