compare_gt_iff_gt — Mathlib

English

In a linear order, compare(a,b) equals Ordering.gt if and only if b < a.

Русский

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

LaTeX

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

Lean4

theorem compare_gt_iff_gt : compare a b = .gt ↔ b < a :=
  by
  rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
  split_ifs <;> simp only [*, lt_irrefl, not_lt_of_gt]
  case _ h₁ h₂ =>
    have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
    rwa [true_iff]

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