Documentation Verification Report

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` `LinearOrder.toDecidableLT`	—	`cmp_eq_gt_iff`
`cmp_eq_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder`	`cmp` `LinearOrder.toDecidableLT`	—	`cmp_eq_lt_iff`

Ordering

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compares_iff_of_compares_impl` 📖	mathematical	`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` `LinearOrder.toDecidableLT`	—	`cmp_compares`
`eq_eq` 📖	—	`Ordering.Compares` `Preorder.toLT`	—	—	`ne_of_lt` `ne_of_gt`
`eq_gt` 📖	—	`Ordering.Compares` `Preorder.toLT`	—	—	`Ordering.swap_eq_iff_eq_swap` `eq_lt` `swap`
`eq_lt` 📖	—	`Ordering.Compares` `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` 📖	—	`Ordering.Compares`	—	—	`Ordering.compares_swap`
`swap` 📖	—	`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`	—	`lt_asymm`
`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`	—	`not_lt` `lt_iff_lt_of_cmp_eq_cmp` `cmp_eq_cmp_symm`
`lt_iff_lt_of_cmp_eq_cmp` 📖	—	`cmp` `Preorder.toLT` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `LinearOrder.toDecidableLT`	—	—	`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