mathlib documentation

core / init.data.ordering.lemmas

source
@[simp]
theorem ordering.ite_eq_lt_distrib (c : Prop) [decidable c] (a b : ordering) :
ite c a b = ordering.lt = ite c (a = ordering.lt) (b = ordering.lt)
source
@[simp]
theorem ordering.ite_eq_eq_distrib (c : Prop) [decidable c] (a b : ordering) :
ite c a b = ordering.eq = ite c (a = ordering.eq) (b = ordering.eq)
source
@[simp]
theorem ordering.ite_eq_gt_distrib (c : Prop) [decidable c] (a b : ordering) :
ite c a b = ordering.gt = ite c (a = ordering.gt) (b = ordering.gt)
source
@[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
source
@[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
source
@[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)