Compare

📁 Source: Mathlib/Order/Compare.lean

Statistics

Metric	Count
Definitions cmpLE, linearOrderOfCompares	2
Theorems cmp_eq_eq, cmp_eq_eq', cmp_eq_gt, cmp_eq_lt, cmp_eq, eq_eq, eq_gt, eq_lt, inj, le_antisymm, le_total, ne_gt, ne_lt, of_swap, swap, compares_iff_of_compares_impl, compares_swap, swap_eq_iff_eq_swap, cmpLE_eq_cmp, cmpLE_ofDual, cmpLE_swap, cmpLE_toDual, cmp_compares, cmp_eq_cmp_symm, cmp_eq_eq_iff, cmp_eq_gt_iff, cmp_eq_lt_iff, cmp_ofDual, cmp_self_eq_eq, cmp_swap, cmp_toDual, eq_iff_eq_of_cmp_eq_cmp, le_iff_le_of_cmp_eq_cmp, lt_iff_lt_of_cmp_eq_cmp, ofDual_compares_ofDual, toDual_compares_toDual	36
Total	38

Eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cmp_eq_eq 📖	mathematical	—	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	cmp_eq_eq_iff
cmp_eq_eq' 📖	mathematical	—	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	cmp_eq_eq

LT.lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cmp_eq_gt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	cmp_eq_gt_iff
cmp_eq_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	cmp_eq_lt_iff

Ordering

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compares_iff_of_compares_impl 📖	mathematical	Compares Preorder.toLT	Compares Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	lt_trichotomy
compares_swap 📖	mathematical	—	Compares	—	—
swap_eq_iff_eq_swap 📖	—	—	—	—	—

Ordering.Compares

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cmp_eq 📖	mathematical	Ordering.Compares Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	cmp_compares
eq_eq 📖	—	Ordering.Compares Preorder.toLT	—	—	ne_of_lt ne_of_gt
eq_gt 📖	mathematical	Ordering.Compares Preorder.toLT	Preorder.toLT	—	Ordering.swap_eq_iff_eq_swap eq_lt swap
eq_lt 📖	mathematical	Ordering.Compares Preorder.toLT	Preorder.toLT	—	ne_of_lt lt_asymm
inj 📖	—	Ordering.Compares Preorder.toLT	—	—	eq_lt eq_eq eq_gt
le_antisymm 📖	—	Ordering.Compares Preorder.toLT Preorder.toLE	—	—	not_le_of_gt
le_total 📖	mathematical	Ordering.Compares Preorder.toLT	Preorder.toLE	—	le_of_lt le_of_eq
ne_gt 📖	mathematical	Ordering.Compares Preorder.toLT	Preorder.toLE	—	Ordering.swap_eq_iff_eq_swap ne_lt swap
ne_lt 📖	mathematical	Ordering.Compares Preorder.toLT	Preorder.toLE	—	not_le_of_gt ge_of_eq le_of_lt
of_swap 📖	mathematical	Ordering.Compares	Ordering.Compares	—	Ordering.compares_swap
swap 📖	mathematical	Ordering.Compares	Ordering.Compares	—	Ordering.compares_swap

(root)

Definitions

Name	Category	Theorems
cmpLE 📖	CompOp	4 math math: cmpLE_ofDual, cmpLE_swap, cmpLE_eq_cmp, cmpLE_toDual
linearOrderOfCompares 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cmpLE_eq_cmp 📖	mathematical	—	cmpLE Preorder.toLE cmp Preorder.toLT	—	total_of
cmpLE_ofDual 📖	mathematical	—	cmpLE DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.instLE	—	—
cmpLE_swap 📖	mathematical	—	cmpLE	—	total_of
cmpLE_toDual 📖	mathematical	—	cmpLE OrderDual OrderDual.instLE DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	—
cmp_compares 📖	mathematical	—	Ordering.Compares Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder cmp LinearOrder.toDecidableLT	—	lt_trichotomy LT.lt.not_gt
cmp_eq_cmp_symm 📖	mathematical	—	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	cmp_swap
cmp_eq_eq_iff 📖	mathematical	—	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	Ordering.Compares.eq_eq cmp_compares
cmp_eq_gt_iff 📖	mathematical	—	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	Ordering.Compares.eq_gt cmp_compares
cmp_eq_lt_iff 📖	mathematical	—	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	Ordering.Compares.eq_lt cmp_compares
cmp_ofDual 📖	mathematical	—	cmp DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.instLT	—	—
cmp_self_eq_eq 📖	mathematical	—	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	cmp_eq_eq_iff
cmp_swap 📖	mathematical	—	cmp Preorder.toLT	—	—
cmp_toDual 📖	mathematical	—	cmp OrderDual OrderDual.instLT DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	—
eq_iff_eq_of_cmp_eq_cmp 📖	—	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	—	—	le_antisymm_iff le_iff_le_of_cmp_eq_cmp cmp_eq_cmp_symm
le_iff_le_of_cmp_eq_cmp 📖	mathematical	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	Preorder.toLE PartialOrder.toPreorder LinearOrder.toPartialOrder	—	not_lt lt_iff_lt_of_cmp_eq_cmp cmp_eq_cmp_symm
lt_iff_lt_of_cmp_eq_cmp 📖	mathematical	cmp Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder LinearOrder.toDecidableLT	Preorder.toLT PartialOrder.toPreorder LinearOrder.toPartialOrder	—	cmp_eq_lt_iff
ofDual_compares_ofDual 📖	mathematical	—	Ordering.Compares DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.instLT	—	—
toDual_compares_toDual 📖	mathematical	—	Ordering.Compares OrderDual OrderDual.instLT DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	—

---

← Back to Index