Documentation Verification Report

Order

📁 Source: Batteries/Classes/Order.lean

Statistics

Metric	Count
Definitions `TotalBLE`, `byKey`, `LawfulBCmp`, `LawfulBOrd`, `LawfulCmp`, `LawfulLECmp`, `LawfulLEOrd`, `LawfulLTCmp`, `LawfulLTOrd`, `LawfulOrd`	10
Theorems `total`, `compareOfLessAndEq_eq_lt`, `eq_lt_iff_lt`, `isLE_iff_le`, `toLawfulBEqCmp`, `toLawfulLECmp`, `toLawfulLTCmp`, `toTransCmp`, `compareOfLessAndEq_of_lt_irrefl`, `compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`, `eq_lt_iff_lt`, `isLE_iff_le`, `toLawfulEqCmp`, `toLawfulLECmp`, `toLawfulLTCmp`, `toTransCmp`, `compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`, `isGE_iff_ge`, `isLE_iff_le`, `ne_gt_iff_le`, `ne_lt_iff_ge`, `toOrientedCmp`, `compareOfLessAndEq_of_irrefl_of_trans_of_antisymm`, `compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`, `eq_compareOfLessAndEq`, `eq_gt_iff_gt`, `eq_lt_iff_lt`, `toOrientedCmp`, `le_iff_ge`, `instOn`, `instOrdLex'`, `compareOfLessAndEq_of_lt_irrefl`, `compareOfLessAndEq_of_irrefl_of_trans_of_antisymm`, `compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`, `ge_trans`, `gt_of_ge_of_gt`, `gt_of_gt_of_ge`, `le_trans`, `lt_of_le_of_lt`, `lt_of_lt_of_le`, `instOn`, `instOrdLex'`, `instLawfulOrdBool`, `instLawfulOrdFin`, `instLawfulOrdInt`, `instLawfulOrdNat`, `instOrientedCmpByKey`, `instOrientedCmpCompareLex_batteries`, `instOrientedCmpCompareOnOfOrientedOrd_batteries`, `instOrientedCmpFlipOrdering_batteries`, `instTransCmpByKey`, `instTransCmpCompareLex_batteries`, `instTransCmpCompareOnOfTransOrd_batteries`, `instTransCmpFlipOrdering_batteries`, `lexOrd_def`	55
Total	65

Batteries

Definitions

Name	Category	Theorems
`TotalBLE` 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compareOfLessAndEq_eq_lt` 📖	—	—	—	—	—

Batteries.TotalBLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`total` 📖	—	—	—	—	—

Ordering

Definitions

Name	Category	Theorems
`byKey` 📖	CompOp	7 math math: `Batteries.RBMap.instIsStrictCutByKeyOfTransCmp`, `Batteries.RBMap.Imp.instIsMonotoneProdByKeyFstMapSnd`, `Batteries.RBMap.toStream_eq`, `Batteries.RBMap.mem_toList`, `Std.instOrientedCmpByKey`, `Batteries.RBMap.val_toList`, `Std.instTransCmpByKey`

Std

Definitions

Name	Category	Theorems
`LawfulBCmp` 📖	CompData	—
`LawfulBOrd` 📖	MathDef	—
`LawfulCmp` 📖	CompData	1 math math: `LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`
`LawfulLECmp` 📖	CompData	3 math math: `LawfulLECmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`, `LawfulCmp.toLawfulLECmp`, `LawfulBCmp.toLawfulLECmp`
`LawfulLEOrd` 📖	MathDef	—
`LawfulLTCmp` 📖	CompData	4 math math: `LawfulCmp.toLawfulLTCmp`, `LawfulBCmp.toLawfulLTCmp`, `LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm`, `LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`
`LawfulLTOrd` 📖	MathDef	1 math math: `String.instLawfulLTOrd`
`LawfulOrd` 📖	MathDef	10 math math: `instLawfulOrdNat`, `instLawfulOrdUInt64`, `instLawfulOrdFin`, `instLawfulOrdUSize`, `instLawfulOrdBool`, `instLawfulOrdUInt16`, `instLawfulOrdInt`, `instLawfulOrdUInt8`, `Char.instLawfulOrd`, `instLawfulOrdUInt32`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLawfulOrdBool` 📖	mathematical	—	`LawfulOrd`	—	—
`instLawfulOrdFin` 📖	mathematical	—	`LawfulOrd`	—	`LawfulLECmp.toOrientedCmp` `LawfulCmp.toLawfulLECmp` `instLawfulOrdNat` `LawfulLTCmp.eq_lt_iff_lt` `LawfulCmp.toLawfulLTCmp` `LawfulLECmp.isLE_iff_le`
`instLawfulOrdInt` 📖	mathematical	—	`LawfulOrd`	—	`LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`
`instLawfulOrdNat` 📖	mathematical	—	`LawfulOrd`	—	`LawfulCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm`
`instOrientedCmpByKey` 📖	mathematical	—	`Ordering.byKey`	—	—
`instOrientedCmpCompareLex_batteries` 📖	—	—	—	—	—
`instOrientedCmpCompareOnOfOrientedOrd_batteries` 📖	—	—	—	—	—
`instOrientedCmpFlipOrdering_batteries` 📖	—	—	—	—	—
`instTransCmpByKey` 📖	mathematical	—	`Ordering.byKey`	—	`instOrientedCmpByKey`
`instTransCmpCompareLex_batteries` 📖	—	—	—	—	—
`instTransCmpCompareOnOfTransOrd_batteries` 📖	—	—	—	—	—
`instTransCmpFlipOrdering_batteries` 📖	—	—	—	—	`instOrientedCmpFlipOrdering_batteries`

Std.LawfulBCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_lt_iff_lt` 📖	—	—	—	—	—
`isLE_iff_le` 📖	—	—	—	—	—
`toLawfulBEqCmp` 📖	—	—	—	—	—
`toLawfulLECmp` 📖	mathematical	—	`Std.LawfulLECmp`	—	`toTransCmp` `isLE_iff_le`
`toLawfulLTCmp` 📖	mathematical	—	`Std.LawfulLTCmp`	—	`toTransCmp` `eq_lt_iff_lt`
`toTransCmp` 📖	—	—	—	—	—

Std.LawfulBEqCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compareOfLessAndEq_of_lt_irrefl` 📖	—	—	—	—	—

Std.LawfulCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm` 📖	mathematical	—	`Std.LawfulCmp`	—	`Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm` `Std.LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm` `Std.LawfulLECmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm` `Std.LawfulLECmp.toOrientedCmp` `Std.LawfulLTCmp.eq_lt_iff_lt` `Std.LawfulLECmp.isLE_iff_le`
`eq_lt_iff_lt` 📖	—	—	—	—	—
`isLE_iff_le` 📖	—	—	—	—	—
`toLawfulEqCmp` 📖	—	—	—	—	—
`toLawfulLECmp` 📖	mathematical	—	`Std.LawfulLECmp`	—	`toTransCmp` `isLE_iff_le`
`toLawfulLTCmp` 📖	mathematical	—	`Std.LawfulLTCmp`	—	`toTransCmp` `eq_lt_iff_lt`
`toTransCmp` 📖	—	—	—	—	—

Std.LawfulLECmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm` 📖	mathematical	—	`Std.LawfulLECmp`	—	`Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm` `Batteries.compareOfLessAndEq_eq_lt`
`isGE_iff_ge` 📖	—	—	—	—	`toOrientedCmp` `isLE_iff_le`
`isLE_iff_le` 📖	—	—	—	—	—
`ne_gt_iff_le` 📖	—	—	—	—	`isLE_iff_le`
`ne_lt_iff_ge` 📖	—	—	—	—	`isGE_iff_ge`
`toOrientedCmp` 📖	—	—	—	—	—

Std.LawfulLTCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compareOfLessAndEq_of_irrefl_of_trans_of_antisymm` 📖	mathematical	—	`Std.LawfulLTCmp`	—	`Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm` `Batteries.compareOfLessAndEq_eq_lt`
`compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm` 📖	mathematical	—	`Std.LawfulLTCmp`	—	`Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm` `Batteries.compareOfLessAndEq_eq_lt`
`eq_compareOfLessAndEq` 📖	—	—	—	—	`eq_lt_iff_lt`
`eq_gt_iff_gt` 📖	—	—	—	—	`toOrientedCmp` `eq_lt_iff_lt`
`eq_lt_iff_lt` 📖	—	—	—	—	—
`toOrientedCmp` 📖	—	—	—	—	—

Std.OrientedCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_iff_ge` 📖	—	—	—	—	—

Std.OrientedOrd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instOn` 📖	—	—	—	—	`Std.instOrientedCmpCompareOnOfOrientedOrd_batteries`
`instOrdLex'` 📖	—	—	—	—	`Std.instOrientedCmpCompareLex_batteries`

Std.ReflCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compareOfLessAndEq_of_lt_irrefl` 📖	—	—	—	—	—

Std.TransCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compareOfLessAndEq_of_irrefl_of_trans_of_antisymm` 📖	—	—	—	—	—
`compareOfLessAndEq_of_irrefl_of_trans_of_not_lt_of_antisymm` 📖	—	—	—	—	`compareOfLessAndEq_of_irrefl_of_trans_of_antisymm`
`ge_trans` 📖	—	—	—	—	—
`gt_of_ge_of_gt` 📖	—	—	—	—	—
`gt_of_gt_of_ge` 📖	—	—	—	—	—
`le_trans` 📖	—	—	—	—	—
`lt_of_le_of_lt` 📖	—	—	—	—	—
`lt_of_lt_of_le` 📖	—	—	—	—	—

Std.TransOrd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instOn` 📖	—	—	—	—	`Std.instTransCmpCompareOnOfTransOrd_batteries`
`instOrdLex'` 📖	—	—	—	—	`Std.instTransCmpCompareLex_batteries`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lexOrd_def` 📖	—	—	—	—	—

---

← Back to Index