cmpUsing_eq_lt — Mathlib

English

Let lt be a strict order. Then cmpUsing lt a b = Ordering.lt if and only if a < b.

Русский

Пусть lt — строгий порядок. Тогда cmpUsing lt a b = Ordering.lt тогда и только тогда, когда a < b.

LaTeX

$$$\\forall a,b,\\ (cmpUsing\\ lt\\ a\\ b = Ordering.lt) \\iff (lt\\ a\\ b)$$$

Lean4

@[simp]
theorem cmpUsing_eq_lt (a b : α) : (cmpUsing lt a b = Ordering.lt) = lt a b := by
  simp only [cmpUsing, Ordering.ite_eq_lt_distrib, ite_self, if_false_right, and_true, reduceCtorEq]

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