compare_eq_iff_eq — Mathlib

English

In a linear order, compare(a,b) equals Ordering.eq if and only if a = b.

Русский

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

LaTeX

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

Lean4

theorem compare_eq_iff_eq : compare a b = .eq ↔ a = b :=
  by
  rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
  split_ifs <;> try simp only
  case _ h => rw [false_iff]; exact ne_iff_lt_or_gt.2 <| .inl h
  case _ _ h => rwa [true_iff]
  case _ _ h => rwa [false_iff]

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