compare_le_iff_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem compare_le_iff_le : compare a b ≠ .gt ↔ a ≤ b :=
  by
  cases h : compare a b
  · simpa using le_of_lt <| compare_lt_iff_lt.1 h
  · simpa using le_of_eq <| compare_eq_iff_eq.1 h
  · simpa using compare_gt_iff_gt.1 h

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