cmpUsing_eq_gt — Mathlib

English

If IsStrictOrder, then cmpUsing lt a b = Ordering.gt iff b < a.

Русский

Если есть строгий порядок, то cmpUsing lt a b = Ordering.gt эквивалентно b < a.

LaTeX

$$$\\forall a,b\\ [IsStrictOrder\\ α\\ lt],\\ (cmpUsing\\ lt\\ a\\ b = Ordering.gt) \\iff (lt b a)$$$

Lean4

@[simp]
theorem cmpUsing_eq_gt [IsStrictOrder α lt] (a b : α) : cmpUsing lt a b = Ordering.gt ↔ lt b a :=
  by
  simp only [cmpUsing, Ordering.ite_eq_gt_distrib, if_false_right, and_true, if_false_left, and_iff_right_iff_imp,
    reduceCtorEq]
  exact fun hba hab ↦ (irrefl a) (_root_.trans hab hba)

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