Basic

📁 Source: Mathlib/Data/Ordering/Basic.lean

Statistics

Metric	Count
Definitions Compares, dthen, cmp, cmpUsing	4
Theorems compares_eq, compares_gt, compares_lt	3
Total	7

Ordering

Definitions

Name	Category	Theorems
Compares 📖	MathDef	14 math math: ONote.cmp_compares, toDual_compares_toDual, StrictAnti.compares, ofDual_compares_ofDual, compares_gt, NONote.cmp_compares, compares_swap, compares_eq, StrictAntiOn.compares, cmp_compares, StrictMonoOn.compares, StrictMono.compares, compare_iff, compares_lt
dthen 📖	CompOp	1 math math: dthen_eq_then

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compares_eq 📖	mathematical	—	Compares	—	—
compares_gt 📖	mathematical	—	Compares	—	—
compares_lt 📖	mathematical	—	Compares	—	—

(root)

Definitions

Name	Category	Theorems
cmp 📖	CompOp	35 math math: Eq.cmp_eq_eq', Ordering.Compares.cmp_eq, Eq.cmp_eq_eq, cmp_add_left, StrictAnti.cmp_map_eq, cmp_self_eq_eq, cmp_eq_cmp_symm, StrictAntiOn.cmp_map_eq, cmp_mul_pos_left, LT.lt.cmp_eq_gt, cmp_toDual, Order.PartialIso.exists_across, cmp_swap, cmp_eq_compare, LT.lt.cmp_eq_lt, Ordinal.cmp_veblen, cmp_mul_right', UpperHalfPlane.cmp_dist_eq_cmp_dist_coe_center, cmp_sub_zero, StrictMonoOn.cmp_map_eq, cmp_eq_eq_iff, cmp_mul_pos_right, Ordinal.cmp_veblenWith, StrictMono.cmp_map_eq, cmp_eq_compareOfLessAndEq, cmp_eq_gt_iff, cmp_eq_lt_iff, cmp_mul_left', cmp_compares, cmp_mul_neg_left, cmp_mul_neg_right, cmp_div_one', cmp_add_right, cmpLE_eq_cmp, cmp_ofDual
cmpUsing 📖	CompOp	3 math math: cmpUsing_eq_gt, cmpUsing_eq_lt, cmpUsing_eq_eq

---

← Back to Index