mathlib documentation

core / init.data.ordering.lemmas

@[simp]
theorem ordering.ite_eq_lt_distrib (c : Prop) [decidable c] (a b : ordering) :

@[simp]
theorem ordering.ite_eq_eq_distrib (c : Prop) [decidable c] (a b : ordering) :

@[simp]
theorem ordering.ite_eq_gt_distrib (c : Prop) [decidable c] (a b : ordering) :

@[simp]
theorem cmp_using_eq_lt {α : Type u} {lt : α → α → Prop} [decidable_rel lt] (a b : α) :
cmp_using lt a b = ordering.lt = lt a b

@[simp]
theorem cmp_using_eq_gt {α : Type u} {lt : α → α → Prop} [decidable_rel lt] [is_strict_order α lt] (a b : α) :
cmp_using lt a b = ordering.gt = lt b a

@[simp]
theorem cmp_using_eq_eq {α : Type u} {lt : α → α → Prop} [decidable_rel lt] (a b : α) :
cmp_using lt a b = ordering.eq = (¬lt a b ¬lt b a)