Comparable

📁 Source: Mathlib/Order/Comparable.lean

Statistics

Metric	Count
Definitions `CompRel`, `decidableRel`, `IncompRel`, `decidableRel`, `linearOrderOfSymmGen`, `instTransAntisymmRelLeCompRel`, `instTransAntisymmRelLeIncompRel`, `instTransCompRelLeAntisymmRel`, `instTransIncompRelLeAntisymmRel`, `linearOrderOfComprel`	10
Theorems `compRel`, `compRel_congr`, `compRel_congr_left`, `compRel_congr_right`, `incompRel_congr`, `incompRel_congr_left`, `incompRel_congr_right`, `not_incompRel`, `trans_compRel`, `trans_incompRel`, `of_antisymmRel_of_compRel`, `of_compRel_of_antisymmRel`, `of_ge`, `of_gt`, `of_le`, `of_lt`, `of_rel`, `of_rel_symm`, `refl`, `rfl`, `trans_antisymmRel`, `ne`, `not_antisymmRel`, `not_ge`, `not_gt`, `not_le`, `not_lt`, `refl`, `rfl`, `trans_antisymmRel`, `compRel`, `not_incompRel`, `compRel`, `compRel_symm`, `not_incompRel`, `compRel`, `compRel_symm`, `not_incompRel`, `antisymmRel_compl`, `antisymmRel_compl_apply`, `compRel_comm`, `compRel_of_total`, `compRel_swap`, `compRel_swap_apply`, `incompRel_comm`, `incompRel_compl`, `incompRel_compl_apply`, `incompRel_of_antisymmRel_of_incompRel`, `incompRel_of_incompRel_of_antisymmRel`, `incompRel_swap`, `incompRel_swap_apply`, `instReflCompRel`, `instReflIncompRelOfIrrefl`, `instSymmCompRel`, `instSymmIncompRel`, `lt_or_antisymmRel_or_gt_or_incompRel`, `lt_or_eq_or_gt_or_incompRel`, `not_compRel_iff`, `not_incompRel_iff`, `not_incompRel_iff_symmGen`, `not_incompRel_of_total`, `not_le_iff_lt_or_incompRel`, `not_symmGen_iff`	63
Total	73

AntisymmRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compRel` 📖	mathematical	`AntisymmRel`	`CompRel`	—	`symmGen`
`compRel_congr` 📖	mathematical	`AntisymmRel` `Preorder.toLE`	`CompRel`	—	`symmGen_congr`
`compRel_congr_left` 📖	mathematical	`AntisymmRel` `Preorder.toLE`	`CompRel`	—	`symmGen_congr_left`
`compRel_congr_right` 📖	mathematical	`AntisymmRel` `Preorder.toLE`	`CompRel`	—	`symmGen_congr_right`
`incompRel_congr` 📖	mathematical	`AntisymmRel` `Preorder.toLE`	`IncompRel`	—	`IncompRel.trans_antisymmRel` `trans_incompRel` `symm`
`incompRel_congr_left` 📖	mathematical	`AntisymmRel` `Preorder.toLE`	`IncompRel`	—	`incompRel_congr` `rfl` `instReflLe`
`incompRel_congr_right` 📖	mathematical	`AntisymmRel` `Preorder.toLE`	`IncompRel`	—	`incompRel_congr` `rfl` `instReflLe`
`not_incompRel` 📖	mathematical	`AntisymmRel`	`IncompRel`	—	—
`trans_compRel` 📖	—	`AntisymmRel` `Preorder.toLE` `CompRel`	—	—	`CompRel.of_antisymmRel_of_compRel`
`trans_incompRel` 📖	—	`AntisymmRel` `Preorder.toLE` `IncompRel`	—	—	`incompRel_of_antisymmRel_of_incompRel`

CompRel

Definitions

Name	Category	Theorems
`decidableRel` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_antisymmRel_of_compRel` 📖	—	`AntisymmRel` `Preorder.toLE` `CompRel`	—	—	`Relation.SymmGen.of_antisymmRel_of_symmGen`
`of_compRel_of_antisymmRel` 📖	—	`CompRel` `Preorder.toLE` `AntisymmRel`	—	—	`Relation.SymmGen.of_symmGen_of_antisymmRel`
`of_ge` 📖	mathematical	—	`CompRel`	—	`Relation.SymmGen.of_ge`
`of_gt` 📖	mathematical	`Preorder.toLT`	`CompRel` `Preorder.toLE`	—	`Relation.SymmGen.of_gt`
`of_le` 📖	mathematical	—	`CompRel`	—	`Relation.SymmGen.of_le`
`of_lt` 📖	mathematical	`Preorder.toLT`	`CompRel` `Preorder.toLE`	—	`Relation.SymmGen.of_lt`
`of_rel` 📖	mathematical	—	`CompRel`	—	`Relation.SymmGen.of_rel`
`of_rel_symm` 📖	mathematical	—	`CompRel`	—	`Relation.SymmGen.of_rel_symm`
`refl` 📖	mathematical	—	`CompRel`	—	`Relation.SymmGen.refl`
`rfl` 📖	mathematical	—	`CompRel`	—	`Relation.SymmGen.rfl`
`trans_antisymmRel` 📖	—	`CompRel` `Preorder.toLE` `AntisymmRel`	—	—	`of_compRel_of_antisymmRel`

IncompRel

Definitions

Name	Category	Theorems
`decidableRel` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ne` 📖	—	`IncompRel`	—	—	`refl_of`
`not_antisymmRel` 📖	mathematical	`IncompRel`	`AntisymmRel`	—	—
`not_ge` 📖	—	`IncompRel`	—	—	—
`not_gt` 📖	mathematical	`IncompRel` `Preorder.toLE`	`Preorder.toLT`	—	`le_of_lt` `not_ge`
`not_le` 📖	—	`IncompRel`	—	—	—
`not_lt` 📖	mathematical	`IncompRel` `Preorder.toLE`	`Preorder.toLT`	—	`le_of_lt` `not_le`
`refl` 📖	mathematical	—	`IncompRel`	—	`AntisymmRel.refl` `Std.Irrefl.compl`
`rfl` 📖	mathematical	—	`IncompRel`	—	`refl`
`trans_antisymmRel` 📖	—	`IncompRel` `Preorder.toLE` `AntisymmRel`	—	—	`incompRel_of_incompRel_of_antisymmRel`

IsTotal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compRel` 📖	mathematical	—	`Relation.SymmGen`	—	`Relation.symmGen_of_total`
`not_incompRel` 📖	mathematical	—	`IncompRel`	—	`not_incompRel_of_total`

LE.le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compRel` 📖	mathematical	—	`CompRel`	—	`CompRel.of_le`
`compRel_symm` 📖	mathematical	—	`CompRel`	—	`CompRel.of_ge`
`not_incompRel` 📖	mathematical	—	`IncompRel`	—	`IncompRel.not_le`

LT.lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compRel` 📖	mathematical	`Preorder.toLT`	`CompRel` `Preorder.toLE`	—	`CompRel.of_lt`
`compRel_symm` 📖	mathematical	`Preorder.toLT`	`CompRel` `Preorder.toLE`	—	`CompRel.of_gt`
`not_incompRel` 📖	mathematical	`Preorder.toLT`	`IncompRel` `Preorder.toLE`	—	`IncompRel.not_lt`

Relation

Definitions

Name	Category	Theorems
`linearOrderOfSymmGen` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`CompRel` 📖	MathDef	24 math math: `LE.le.compRel`, `CompRel.of_le`, `AntisymmRel.compRel_congr_right`, `CompRel.of_rel`, `instSymmCompRel`, `CompRel.of_rel_symm`, `CompRel.rfl`, `AntisymmRel.compRel`, `LT.lt.compRel`, `not_compRel_iff`, `AntisymmRel.compRel_congr_left`, `LE.le.compRel_symm`, `compRel_comm`, `AntisymmRel.compRel_congr`, `not_incompRel_iff`, `CompRel.refl`, `LT.lt.compRel_symm`, `CompRel.of_gt`, `compRel_swap`, `CompRel.of_ge`, `compRel_swap_apply`, `instReflCompRel`, `CompRel.of_lt`, `compRel_of_total`
`IncompRel` 📖	MathDef	26 math math: `AntisymmRel.incompRel_congr`, `IncompRel.rfl`, `instSymmIncompRel`, `incompRel_swap`, `AntisymmRel.not_incompRel`, `not_incompRel_of_total`, `IncompRel.refl`, `LT.lt.not_incompRel`, `not_compRel_iff`, `antisymmRel_compl_apply`, `not_le_iff_lt_or_incompRel`, `AntisymmRel.incompRel_congr_left`, `AntisymmRel.incompRel_congr_right`, `lt_or_eq_or_gt_or_incompRel`, `not_incompRel_iff`, `incompRel_swap_apply`, `incompRel_compl_apply`, `antisymmRel_compl`, `lt_or_antisymmRel_or_gt_or_incompRel`, `instReflIncompRelOfIrrefl`, `incompRel_comm`, `not_symmGen_iff`, `LE.le.not_incompRel`, `incompRel_compl`, `IsTotal.not_incompRel`, `not_incompRel_iff_symmGen`
`instTransAntisymmRelLeCompRel` 📖	CompOp	—
`instTransAntisymmRelLeIncompRel` 📖	CompOp	—
`instTransCompRelLeAntisymmRel` 📖	CompOp	—
`instTransIncompRelLeAntisymmRel` 📖	CompOp	—
`linearOrderOfComprel` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antisymmRel_compl` 📖	mathematical	—	`AntisymmRel` `Compl.compl` `Pi.instCompl` `Prop.instCompl` `IncompRel`	—	—
`antisymmRel_compl_apply` 📖	mathematical	—	`AntisymmRel` `Compl.compl` `Pi.instCompl` `Prop.instCompl` `IncompRel`	—	—
`compRel_comm` 📖	mathematical	—	`CompRel`	—	`Relation.symmGen_comm`
`compRel_of_total` 📖	mathematical	—	`CompRel`	—	`Relation.symmGen_of_total`
`compRel_swap` 📖	mathematical	—	`CompRel` `Function.swap`	—	`Relation.symmGen_swap`
`compRel_swap_apply` 📖	mathematical	—	`CompRel` `Function.swap`	—	`Relation.symmGen_swap_apply`
`incompRel_comm` 📖	mathematical	—	`IncompRel`	—	`comm` `instSymmIncompRel`
`incompRel_compl` 📖	mathematical	—	`IncompRel` `Compl.compl` `Pi.instCompl` `Prop.instCompl` `AntisymmRel`	—	—
`incompRel_compl_apply` 📖	mathematical	—	`IncompRel` `Compl.compl` `Pi.instCompl` `Prop.instCompl` `AntisymmRel`	—	`incompRel_compl`
`incompRel_of_antisymmRel_of_incompRel` 📖	—	`AntisymmRel` `Preorder.toLE` `IncompRel`	—	—	`IncompRel.symm` `IncompRel.trans_antisymmRel` `AntisymmRel.symm`
`incompRel_of_incompRel_of_antisymmRel` 📖	—	`IncompRel` `Preorder.toLE` `AntisymmRel`	—	—	`IncompRel.not_le` `LE.le.trans` `AntisymmRel.ge` `IncompRel.not_ge` `AntisymmRel.le`
`incompRel_swap` 📖	mathematical	—	`IncompRel` `Function.swap`	—	`antisymmRel_swap`
`incompRel_swap_apply` 📖	mathematical	—	`IncompRel` `Function.swap`	—	`antisymmRel_swap_apply`
`instReflCompRel` 📖	mathematical	—	`CompRel`	—	`Relation.SymmGen.instRefl`
`instReflIncompRelOfIrrefl` 📖	mathematical	—	`IncompRel`	—	`IncompRel.refl`
`instSymmCompRel` 📖	mathematical	—	`CompRel`	—	`Relation.SymmGen.instSymm`
`instSymmIncompRel` 📖	mathematical	—	`IncompRel`	—	`IncompRel.symm`
`lt_or_antisymmRel_or_gt_or_incompRel` 📖	mathematical	—	`Preorder.toLT` `AntisymmRel` `Preorder.toLE` `IncompRel`	—	—
`lt_or_eq_or_gt_or_incompRel` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `IncompRel` `Preorder.toLE`	—	`instReflLe` `instAntisymmLe` `lt_or_antisymmRel_or_gt_or_incompRel`
`not_compRel_iff` 📖	mathematical	—	`CompRel` `IncompRel`	—	`not_symmGen_iff`
`not_incompRel_iff` 📖	mathematical	—	`IncompRel` `CompRel`	—	`not_incompRel_iff_symmGen`
`not_incompRel_iff_symmGen` 📖	mathematical	—	`IncompRel` `Relation.SymmGen`	—	`not_symmGen_iff`
`not_incompRel_of_total` 📖	mathematical	—	`IncompRel`	—	`not_incompRel_iff_symmGen` `Relation.symmGen_of_total`
`not_le_iff_lt_or_incompRel` 📖	mathematical	—	`Preorder.toLE` `Preorder.toLT` `IncompRel`	—	`lt_iff_le_not_ge` `IncompRel.eq_1`
`not_symmGen_iff` 📖	mathematical	—	`Relation.SymmGen` `IncompRel`	—	—

---

← Back to Index