Documentation Verification Report

Deprecated

📁 Source: Batteries/Classes/Deprecated.lean

Statistics

Metric	Count
Definitions `BEqCmp`, `BEqOrd`, `LECmp`, `LEOrd`, `LTCmp`, `LTOrd`, `LawfulCmp`, `LawfulOrd`, `OrientedCmp`, `OrientedOrd`, `TransCmp`, `TransOrd`	12
Theorems `cmp_iff_beq`, `cmp_iff_eq`, `compareOfLessAndEq`, `cmp_iff_ge`, `cmp_iff_le`, `compareOfLessAndEq`, `toOrientedCmp`, `cmp_iff_gt`, `cmp_iff_lt`, `compareOfLessAndEq`, `compareOfLessAndEq_of_le`, `eq_compareOfLessAndEq`, `toOrientedCmp`, `cmp_iff_le`, `cmp_iff_lt`, `compareOfLessAndEq`, `toBEqCmp`, `toLECmp`, `toLTCmp`, `toTransCmp`, `cmp_eq_eq_symm`, `cmp_eq_gt`, `cmp_ne_gt`, `cmp_refl`, `gt_asymm`, `lt_asymm`, `symm`, `instLexOrd`, `instOn`, `instOpposite`, `instOrdLex`, `instOrdLex'`, `cmp_congr_left`, `cmp_congr_left'`, `cmp_congr_right`, `compareOfLessAndEq`, `compareOfLessAndEq_of_le`, `ge_trans`, `gt_trans`, `le_lt_trans`, `le_trans`, `lt_le_trans`, `lt_trans`, `toOrientedCmp`, `instLexOrd`, `instOn`, `instOpposite`, `instOrdLex`, `instOrdLex'`, `instOrientedCmpCompareLex`, `instOrientedCmpCompareOnOfOrientedOrd`, `instOrientedCmpFlipOrdering`, `instTransCmpCompareLex`, `instTransCmpCompareOnOfTransOrd`, `instTransCmpFlipOrdering`	55
Total	67

Batteries

Definitions

Name	Category	Theorems
`BEqCmp` 📖	CompData	2 math math: `BEqCmp.compareOfLessAndEq`, `LawfulCmp.toBEqCmp`
`BEqOrd` 📖	MathDef	—
`LECmp` 📖	CompData	2 math math: `LECmp.compareOfLessAndEq`, `LawfulCmp.toLECmp`
`LEOrd` 📖	MathDef	—
`LTCmp` 📖	CompData	3 math math: `LTCmp.compareOfLessAndEq`, `LTCmp.compareOfLessAndEq_of_le`, `LawfulCmp.toLTCmp`
`LTOrd` 📖	MathDef	—
`LawfulCmp` 📖	CompData	1 math math: `LawfulCmp.compareOfLessAndEq`
`LawfulOrd` 📖	MathDef	—
`OrientedCmp` 📖	CompData	6 math math: `instOrientedCmpCompareOnOfOrientedOrd`, `instOrientedCmpCompareLex`, `LTCmp.toOrientedCmp`, `instOrientedCmpFlipOrdering`, `TransCmp.toOrientedCmp`, `LECmp.toOrientedCmp`
`OrientedOrd` 📖	MathDef	5 math math: `OrientedOrd.instOrdLex'`, `OrientedOrd.instOpposite`, `OrientedOrd.instLexOrd`, `OrientedOrd.instOrdLex`, `OrientedOrd.instOn`
`TransCmp` 📖	CompData	6 math math: `TransCmp.compareOfLessAndEq`, `TransCmp.compareOfLessAndEq_of_le`, `LawfulCmp.toTransCmp`, `instTransCmpCompareOnOfTransOrd`, `instTransCmpFlipOrdering`, `instTransCmpCompareLex`
`TransOrd` 📖	MathDef	5 math math: `TransOrd.instOpposite`, `TransOrd.instOrdLex`, `TransOrd.instOn`, `TransOrd.instOrdLex'`, `TransOrd.instLexOrd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instOrientedCmpCompareLex` 📖	mathematical	—	`OrientedCmp`	—	`OrientedCmp.symm`
`instOrientedCmpCompareOnOfOrientedOrd` 📖	mathematical	—	`OrientedCmp`	—	`OrientedCmp.symm`
`instOrientedCmpFlipOrdering` 📖	mathematical	—	`OrientedCmp`	—	`OrientedCmp.symm`
`instTransCmpCompareLex` 📖	mathematical	—	`TransCmp`	—	`instOrientedCmpCompareLex` `TransCmp.toOrientedCmp` `TransCmp.le_trans` `TransCmp.cmp_congr_left` `OrientedCmp.cmp_eq_gt`
`instTransCmpCompareOnOfTransOrd` 📖	mathematical	—	`TransCmp`	—	`instOrientedCmpCompareOnOfOrientedOrd` `TransCmp.toOrientedCmp` `TransCmp.le_trans`
`instTransCmpFlipOrdering` 📖	mathematical	—	`TransCmp`	—	`instOrientedCmpFlipOrdering` `TransCmp.toOrientedCmp` `TransCmp.le_trans`

Batteries.BEqCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cmp_iff_beq` 📖	—	—	—	—	—
`cmp_iff_eq` 📖	—	—	—	—	—
`compareOfLessAndEq` 📖	mathematical	—	`Batteries.BEqCmp`	—	—

Batteries.LECmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cmp_iff_ge` 📖	—	—	—	—	`Batteries.OrientedCmp.cmp_ne_gt` `toOrientedCmp` `cmp_iff_le`
`cmp_iff_le` 📖	—	—	—	—	—
`compareOfLessAndEq` 📖	mathematical	—	`Batteries.LECmp`	—	`Batteries.TransCmp.compareOfLessAndEq_of_le` `Batteries.TransCmp.toOrientedCmp` `Batteries.OrientedCmp.cmp_ne_gt` `Batteries.compareOfLessAndEq_eq_lt`
`toOrientedCmp` 📖	mathematical	—	`Batteries.OrientedCmp`	—	—

Batteries.LTCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cmp_iff_gt` 📖	—	—	—	—	`Batteries.OrientedCmp.cmp_eq_gt` `toOrientedCmp` `cmp_iff_lt`
`cmp_iff_lt` 📖	—	—	—	—	—
`compareOfLessAndEq` 📖	mathematical	—	`Batteries.LTCmp`	—	`Batteries.TransCmp.compareOfLessAndEq` `Batteries.TransCmp.toOrientedCmp` `Batteries.compareOfLessAndEq_eq_lt`
`compareOfLessAndEq_of_le` 📖	mathematical	—	`Batteries.LTCmp`	—	`Batteries.TransCmp.compareOfLessAndEq_of_le` `Batteries.TransCmp.toOrientedCmp` `Batteries.compareOfLessAndEq_eq_lt`
`eq_compareOfLessAndEq` 📖	—	—	—	—	`cmp_iff_lt` `Batteries.BEqCmp.cmp_iff_eq`
`toOrientedCmp` 📖	mathematical	—	`Batteries.OrientedCmp`	—	—

Batteries.LawfulCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cmp_iff_le` 📖	—	—	—	—	—
`cmp_iff_lt` 📖	—	—	—	—	—
`compareOfLessAndEq` 📖	mathematical	—	`Batteries.LawfulCmp`	—	`Batteries.TransCmp.compareOfLessAndEq_of_le` `Batteries.LTCmp.compareOfLessAndEq_of_le` `Batteries.LECmp.compareOfLessAndEq` `Batteries.BEqCmp.compareOfLessAndEq` `Batteries.LTCmp.cmp_iff_lt` `Batteries.LECmp.cmp_iff_le`
`toBEqCmp` 📖	mathematical	—	`Batteries.BEqCmp`	—	—
`toLECmp` 📖	mathematical	—	`Batteries.LECmp`	—	`Batteries.TransCmp.toOrientedCmp` `toTransCmp` `cmp_iff_le`
`toLTCmp` 📖	mathematical	—	`Batteries.LTCmp`	—	`Batteries.TransCmp.toOrientedCmp` `toTransCmp` `cmp_iff_lt`
`toTransCmp` 📖	mathematical	—	`Batteries.TransCmp`	—	—

Batteries.OrientedCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cmp_eq_eq_symm` 📖	—	—	—	—	`symm`
`cmp_eq_gt` 📖	—	—	—	—	`symm`
`cmp_ne_gt` 📖	—	—	—	—	`cmp_eq_gt`
`cmp_refl` 📖	—	—	—	—	`cmp_eq_gt`
`gt_asymm` 📖	—	—	—	—	`cmp_eq_gt` `lt_asymm`
`lt_asymm` 📖	—	—	—	—	`cmp_eq_gt`
`symm` 📖	—	—	—	—	—

Batteries.OrientedOrd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLexOrd` 📖	mathematical	—	`Batteries.OrientedOrd`	—	`eq_1` `lexOrd_def` `Batteries.instOrientedCmpCompareLex` `Batteries.instOrientedCmpCompareOnOfOrientedOrd`
`instOn` 📖	mathematical	—	`Batteries.OrientedOrd`	—	`Batteries.instOrientedCmpCompareOnOfOrientedOrd`
`instOpposite` 📖	mathematical	—	`Batteries.OrientedOrd`	—	`Batteries.OrientedCmp.symm`
`instOrdLex` 📖	mathematical	—	`Batteries.OrientedOrd`	—	`instLexOrd`
`instOrdLex'` 📖	mathematical	—	`Batteries.OrientedOrd`	—	`Batteries.instOrientedCmpCompareLex`

Batteries.TransCmp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cmp_congr_left` 📖	—	—	—	—	`ge_trans` `Batteries.OrientedCmp.cmp_eq_eq_symm` `toOrientedCmp` `le_trans`
`cmp_congr_left'` 📖	—	—	—	—	`cmp_congr_left`
`cmp_congr_right` 📖	—	—	—	—	`Batteries.OrientedCmp.symm` `toOrientedCmp` `cmp_congr_left`
`compareOfLessAndEq` 📖	mathematical	—	`Batteries.TransCmp`	—	`Batteries.OrientedCmp.cmp_eq_gt` `Batteries.compareOfLessAndEq_eq_lt`
`compareOfLessAndEq_of_le` 📖	mathematical	—	`Batteries.TransCmp`	—	`compareOfLessAndEq`
`ge_trans` 📖	—	—	—	—	`le_trans` `toOrientedCmp`
`gt_trans` 📖	—	—	—	—	`Batteries.OrientedCmp.cmp_eq_gt` `toOrientedCmp` `lt_trans`
`le_lt_trans` 📖	—	—	—	—	`ge_trans` `Batteries.OrientedCmp.cmp_eq_gt` `toOrientedCmp`
`le_trans` 📖	—	—	—	—	—
`lt_le_trans` 📖	—	—	—	—	`ge_trans` `Batteries.OrientedCmp.cmp_eq_gt` `toOrientedCmp`
`lt_trans` 📖	—	—	—	—	`le_lt_trans` `Batteries.OrientedCmp.gt_asymm` `toOrientedCmp` `Batteries.OrientedCmp.cmp_eq_gt`
`toOrientedCmp` 📖	mathematical	—	`Batteries.OrientedCmp`	—	—

Batteries.TransOrd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLexOrd` 📖	mathematical	—	`Batteries.TransOrd`	—	`eq_1` `lexOrd_def` `Batteries.instTransCmpCompareLex` `Batteries.instTransCmpCompareOnOfTransOrd`
`instOn` 📖	mathematical	—	`Batteries.TransOrd`	—	`Batteries.instTransCmpCompareOnOfTransOrd`
`instOpposite` 📖	mathematical	—	`Batteries.TransOrd`	—	`Batteries.OrientedOrd.instOpposite` `Batteries.TransCmp.toOrientedCmp` `Batteries.TransCmp.le_trans`
`instOrdLex` 📖	mathematical	—	`Batteries.TransOrd`	—	`instLexOrd`
`instOrdLex'` 📖	mathematical	—	`Batteries.TransOrd`	—	`Batteries.instTransCmpCompareLex`

---

← Back to Index