Documentation Verification Report

Grade

📁 Source: Mathlib/Order/Grade.lean

Statistics

Metric	Count
Definitions `instGradeBoundedOrderSubtypeMem`, `instGradeMaxOrderSubtypeMem`, `instGradeMinOrderSubtypeMem`, `instGradeOrderSubtypeMem`, `GradeBoundedOrder`, `liftLeft`, `liftRight`, `toGradeMaxOrder`, `toGradeMinOrder`, `GradeMaxOrder`, `liftLeft`, `liftRight`, `toGradeOrder`, `GradeMinOrder`, `finToNat`, `liftLeft`, `liftRight`, `toGradeOrder`, `GradeOrder`, `finToNat`, `grade`, `liftLeft`, `liftRight`, `natToInt`, `gradeMaxOrder`, `gradeMinOrder`, `gradeOrder`, `toGradeBoundedOrder`, `grade`, `instGradeBoundedOrderOrderDual`	30
Theorems `grade`, `coe_covBy_coe`, `coe_wcovBy_coe`, `grade_coe`, `isMax_coe`, `isMin_coe`, `isMax_grade`, `isMax_grade`, `isMin_grade`, `covBy_grade`, `grade_strictMono`, `wellFoundedGT`, `wellFoundedLT`, `grade`, `grade`, `covBy_iff_lt_covBy_grade`, `grade_bot`, `grade_covBy_grade_iff`, `grade_eq_grade_iff`, `grade_injective`, `grade_le_grade_iff`, `grade_lt_grade_iff`, `grade_mono`, `grade_ne_grade_iff`, `grade_ofDual`, `grade_self`, `grade_strictMono`, `grade_toDual`, `grade_top`, `instWellFoundedGTOfGradeOrderOrderDualNat`, `instWellFoundedLTOfGradeOrderNat`, `isMax_grade_iff`, `isMin_grade_iff`	33
Total	63

CovBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`grade` 📖	mathematical	`CovBy` `Preorder.toLT`	`grade`	—	`GradeOrder.covBy_grade`

Flag

Definitions

Name	Category	Theorems
`instGradeBoundedOrderSubtypeMem` 📖	CompOp	—
`instGradeMaxOrderSubtypeMem` 📖	CompOp	—
`instGradeMinOrderSubtypeMem` 📖	CompOp	—
`instGradeOrderSubtypeMem` 📖	CompOp	1 math math: `grade_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_covBy_coe` 📖	mathematical	—	`CovBy` `Preorder.toLT` `PartialOrder.toPreorder` `Flag` `Preorder.toLE` `SetLike.instMembership` `instSetLike`	—	—
`coe_wcovBy_coe` 📖	mathematical	—	`WCovBy` `PartialOrder.toPreorder` `Flag` `Preorder.toLE` `SetLike.instMembership` `instSetLike` `Subtype.preorder`	—	`mem_iff_forall_le_or_ge` `le_or_gt` `LE.le.trans` `Subtype.coe_le_coe` `LT.lt.le`
`grade_coe` 📖	mathematical	—	`grade` `PartialOrder.toPreorder` `Flag` `Preorder.toLE` `SetLike.instMembership` `instSetLike` `Subtype.preorder` `instGradeOrderSubtypeMem`	—	—
`isMax_coe` 📖	mathematical	—	`IsMax` `Preorder.toLE` `PartialOrder.toPreorder` `Flag` `SetLike.instMembership` `instSetLike`	—	`mem_iff_forall_le_or_ge` `LE.le.trans'` `IsMax.isTop` `SemilatticeSup.instIsDirectedOrder`
`isMin_coe` 📖	mathematical	—	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `Flag` `SetLike.instMembership` `instSetLike`	—	`mem_iff_forall_le_or_ge` `LE.le.trans` `IsMin.isBot` `SemilatticeInf.instIsCodirectedOrder`

GradeBoundedOrder

Definitions

Name	Category	Theorems
`liftLeft` 📖	CompOp	—
`liftRight` 📖	CompOp	—
`toGradeMaxOrder` 📖	CompOp	1 math math: `grade_self`
`toGradeMinOrder` 📖	CompOp	1 math math: `isMax_grade`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMax_grade` 📖	mathematical	`IsMax` `Preorder.toLE`	`GradeOrder.grade` `GradeMinOrder.toGradeOrder` `toGradeMinOrder`	—	—

GradeMaxOrder

Definitions

Name	Category	Theorems
`liftLeft` 📖	CompOp	—
`liftRight` 📖	CompOp	—
`toGradeOrder` 📖	CompOp	5 math math: `isMax_grade_iff`, `grade_top`, `IsMax.grade`, `grade_self`, `isMax_grade`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMax_grade` 📖	mathematical	`IsMax` `Preorder.toLE`	`GradeOrder.grade` `toGradeOrder`	—	—

GradeMinOrder

Definitions

Name	Category	Theorems
`finToNat` 📖	CompOp	—
`liftLeft` 📖	CompOp	—
`liftRight` 📖	CompOp	—
`toGradeOrder` 📖	CompOp	9 math math: `grade_bot`, `Finset.grade_eq`, `exists_nat_orderEmbedding_of_forall_covby_finite`, `GradeBoundedOrder.isMax_grade`, `isMin_grade`, `IsMin.grade`, `Multiset.grade_eq`, `Finset.grade_multiset_eq`, `isMin_grade_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMin_grade` 📖	mathematical	`IsMin` `Preorder.toLE`	`GradeOrder.grade` `toGradeOrder`	—	—

GradeOrder

Definitions

Name	Category	Theorems
`finToNat` 📖	CompOp	—
`grade` 📖	CompOp	5 math math: `GradeBoundedOrder.isMax_grade`, `GradeMinOrder.isMin_grade`, `covBy_grade`, `grade_strictMono`, `GradeMaxOrder.isMax_grade`
`liftLeft` 📖	CompOp	—
`liftRight` 📖	CompOp	—
`natToInt` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`covBy_grade` 📖	mathematical	`CovBy` `Preorder.toLT`	`grade`	—	—
`grade_strictMono` 📖	mathematical	—	`StrictMono` `grade`	—	—
`wellFoundedGT` 📖	mathematical	—	`WellFoundedGT` `Preorder.toLT`	—	`StrictMono.wellFoundedGT` `grade_strictMono`
`wellFoundedLT` 📖	mathematical	—	`WellFoundedLT` `Preorder.toLT`	—	`StrictMono.wellFoundedLT` `grade_strictMono`

IsMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`grade` 📖	mathematical	`IsMax` `Preorder.toLE`	`grade` `GradeMaxOrder.toGradeOrder`	—	`GradeMaxOrder.isMax_grade`

IsMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`grade` 📖	mathematical	`IsMin` `Preorder.toLE`	`grade` `GradeMinOrder.toGradeOrder`	—	`GradeMinOrder.isMin_grade`

OrderDual

Definitions

Name	Category	Theorems
`gradeMaxOrder` 📖	CompOp	—
`gradeMinOrder` 📖	CompOp	—
`gradeOrder` 📖	CompOp	2 math math: `grade_ofDual`, `grade_toDual`

Preorder

Definitions

Name	Category	Theorems
`toGradeBoundedOrder` 📖	CompOp	1 math math: `grade_self`

(root)

Definitions

Name	Category	Theorems
`GradeBoundedOrder` 📖	CompData	—
`GradeMaxOrder` 📖	CompData	—
`GradeMinOrder` 📖	CompData	—
`GradeOrder` 📖	CompData	—
`grade` 📖	CompOp	23 math math: `covBy_iff_lt_covBy_grade`, `grade_bot`, `Finset.grade_eq`, `grade_strictMono`, `GradeMinOrder.exists_nat_orderEmbedding_of_forall_covby_finite`, `grade_le_grade_iff`, `isMax_grade_iff`, `grade_eq_grade_iff`, `grade_top`, `grade_lt_grade_iff`, `grade_mono`, `IsMin.grade`, `Multiset.grade_eq`, `IsMax.grade`, `Flag.grade_coe`, `Finset.grade_multiset_eq`, `grade_injective`, `CovBy.grade`, `grade_ofDual`, `grade_covBy_grade_iff`, `grade_toDual`, `grade_self`, `isMin_grade_iff`
`instGradeBoundedOrderOrderDual` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`covBy_iff_lt_covBy_grade` 📖	mathematical	—	`CovBy` `Preorder.toLT` `grade`	—	`CovBy.grade` `grade_strictMono`
`grade_bot` 📖	mathematical	—	`grade` `PartialOrder.toPreorder` `GradeMinOrder.toGradeOrder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`IsMin.eq_bot` `IsMin.grade` `isMin_bot`
`grade_covBy_grade_iff` 📖	mathematical	—	`CovBy` `Preorder.toLT` `grade` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`covBy_iff_lt_covBy_grade` `grade_lt_grade_iff`
`grade_eq_grade_iff` 📖	mathematical	—	`grade` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`grade_injective`
`grade_injective` 📖	mathematical	—	`grade` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`StrictMono.injective` `grade_strictMono`
`grade_le_grade_iff` 📖	mathematical	—	`Preorder.toLE` `grade` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`StrictMono.le_iff_le` `grade_strictMono`
`grade_lt_grade_iff` 📖	mathematical	—	`Preorder.toLT` `grade` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`StrictMono.lt_iff_lt` `grade_strictMono`
`grade_mono` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `grade`	—	`StrictMono.monotone` `grade_strictMono`
`grade_ne_grade_iff` 📖	—	—	—	—	`grade_injective`
`grade_ofDual` 📖	mathematical	—	`grade` `DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderDual.instPreorder` `OrderDual.gradeOrder`	—	—
`grade_self` 📖	mathematical	—	`grade` `GradeMaxOrder.toGradeOrder` `GradeBoundedOrder.toGradeMaxOrder` `Preorder.toGradeBoundedOrder`	—	—
`grade_strictMono` 📖	mathematical	—	`StrictMono` `grade`	—	`GradeOrder.grade_strictMono`
`grade_toDual` 📖	mathematical	—	`grade` `OrderDual` `OrderDual.instPreorder` `OrderDual.gradeOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`grade_top` 📖	mathematical	—	`grade` `PartialOrder.toPreorder` `GradeMaxOrder.toGradeOrder` `Top.top` `OrderTop.toTop` `Preorder.toLE`	—	`IsMax.eq_top` `IsMax.grade` `isMax_top`
`instWellFoundedGTOfGradeOrderOrderDualNat` 📖	mathematical	—	`WellFoundedGT` `Preorder.toLT`	—	`GradeOrder.wellFoundedGT` `IsWellOrder.toIsWellFounded` `isWellOrder_gt` `instWellFoundedGTOrderDualOfWellFoundedLT` `instWellFoundedLTNat`
`instWellFoundedLTOfGradeOrderNat` 📖	mathematical	—	`WellFoundedLT` `Preorder.toLT`	—	`GradeOrder.wellFoundedLT` `instWellFoundedLTNat`
`isMax_grade_iff` 📖	mathematical	—	`IsMax` `Preorder.toLE` `grade` `GradeMaxOrder.toGradeOrder`	—	`StrictMono.isMax_of_apply` `grade_strictMono` `IsMax.grade`
`isMin_grade_iff` 📖	mathematical	—	`IsMin` `Preorder.toLE` `grade` `GradeMinOrder.toGradeOrder`	—	`StrictMono.isMin_of_apply` `grade_strictMono` `IsMin.grade`

---

← Back to Index