Documentation Verification Report

Lex

📁 Source: Mathlib/Data/DFinsupp/Lex.lean

Statistics

Metric	Count
Definitions `decidableLE`, `decidableLT`, `linearOrder`, `orderBot`, `partialOrder`, `Lex`, `decidableLE`, `decidableLT`, `linearOrder`, `orderBot`, `partialOrder`, `instLTColex`, `instLTLex`	13
Theorems `addLeftMono`, `addLeftStrictMono`, `addRightMono`, `addRightStrictMono`, `isOrderedAddMonoid`, `isOrderedCancelAddMonoid`, `isStrictOrder`, `le_iff_of_unique`, `lt_iff`, `total_le`, `addLeftMono`, `addLeftStrictMono`, `addRightMono`, `addRightStrictMono`, `isOrderedAddMonoid`, `isOrderedCancelAddMonoid`, `isStrictOrder`, `le_iff_of_unique`, `lt_iff`, `lt_iff_of_unique`, `total_le`, `colex_lt_iff_of_unique`, `lex_def`, `lex_iff_of_unique`, `lex_le_iff_of_unique`, `lex_lt_iff`, `lex_lt_iff_of_unique`, `lex_lt_of_lt`, `lex_lt_of_lt_of_preorder`, `lt_of_forall_lt_of_lt`, `toColex_monotone`, `toLex_monotone`, `lex_eq_dfinsupp_lex`	33
Total	46

DFinsupp

Definitions

Name	Category	Theorems
`Lex` 📖	MathDef	11 math math: `Lex.acc_zero`, `Lex.wellFounded`, `lex_def`, `Pi.lex_eq_dfinsupp_lex`, `lex_iff_of_unique`, `lex_fibration`, `Lex.wellFounded'`, `Lex.acc_single`, `Finsupp.lex_eq_invImage_dfinsupp_lex`, `Lex.acc`, `Lex.wellFounded_of_finite`
`instLTColex` 📖	CompOp	7 math math: `Colex.wellFoundedLT`, `colex_lt_iff_of_unique`, `Colex.lt_iff`, `Colex.wellFoundedLT_of_finite`, `Colex.addLeftStrictMono`, `Colex.addRightStrictMono`, `Colex.isStrictOrder`
`instLTLex` 📖	CompOp	10 math math: `lex_lt_iff_of_unique`, `lt_of_forall_lt_of_lt`, `lex_lt_iff`, `Lex.addLeftStrictMono`, `Lex.addRightStrictMono`, `Lex.lt_iff_of_unique`, `Lex.wellFoundedLT_of_finite`, `Lex.isStrictOrder`, `Lex.wellFoundedLT`, `Lex.lt_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`colex_lt_iff_of_unique` 📖	mathematical	—	`Colex` `DFinsupp` `instLTColex` `Preorder.toLT` `Unique.instInhabited` `DFunLike.coe` `instDFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex`	—	`lex_iff_of_unique` `instIrreflGt`
`lex_def` 📖	mathematical	—	`Lex` `DFunLike.coe` `DFinsupp` `instDFunLike`	—	—
`lex_iff_of_unique` 📖	mathematical	—	`Lex` `Unique.instInhabited` `DFunLike.coe` `DFinsupp` `instDFunLike`	—	`Pi.lex_iff_of_unique`
`lex_le_iff_of_unique` 📖	mathematical	—	`Lex` `DFinsupp` `Preorder.toLE` `PartialOrder.toPreorder` `Lex.partialOrder` `Unique.instInhabited` `DFunLike.coe` `instDFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`Lex.le_iff_of_unique`
`lex_lt_iff` 📖	mathematical	—	`Lex` `DFinsupp` `instLTLex` `DFunLike.coe` `instDFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`Lex.lt_iff`
`lex_lt_iff_of_unique` 📖	mathematical	—	`Lex` `DFinsupp` `instLTLex` `Preorder.toLT` `Unique.instInhabited` `DFunLike.coe` `instDFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`Lex.lt_iff_of_unique`
`lex_lt_of_lt` 📖	mathematical	`DFinsupp` `Preorder.toLT` `instPreorder` `PartialOrder.toPreorder`	`Pi.Lex` `DFunLike.coe` `instDFunLike`	—	`lex_lt_of_lt_of_preorder`
`lex_lt_of_lt_of_preorder` 📖	mathematical	`DFinsupp` `Preorder.toLT` `instPreorder`	`Preorder.toLE` `DFunLike.coe` `instDFunLike`	—	`Pi.lt_def` `Set.Finite.wellFoundedOn` `Finset.finite_toSet` `WellFounded.has_min` `mem_neLocus` `LT.lt.ne` `of_not_not` `ne_of_not_le` `LE.le.lt_of_not_ge`
`lt_of_forall_lt_of_lt` 📖	mathematical	`DFunLike.coe` `DFinsupp` `instDFunLike` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `Preorder.toLT` `PartialOrder.toPreorder`	`instLTLex` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—
`toColex_monotone` 📖	mathematical	—	`Monotone` `DFinsupp` `Colex` `instPreorder` `PartialOrder.toPreorder` `Colex.partialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	`toLex_monotone`
`toLex_monotone` 📖	mathematical	—	`Monotone` `DFinsupp` `Lex` `instPreorder` `PartialOrder.toPreorder` `Lex.partialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`le_of_lt_or_eq` `nonempty_neLocus_iff` `notMem_neLocus` `LE.le.not_gt` `Finset.min'_le` `LE.le.lt_of_ne` `mem_neLocus` `Finset.min'_mem`

DFinsupp.Colex

Definitions

Name	Category	Theorems
`decidableLE` 📖	CompOp	—
`decidableLT` 📖	CompOp	—
`linearOrder` 📖	CompOp	—
`orderBot` 📖	CompOp	—
`partialOrder` 📖	CompOp	7 math math: `isOrderedCancelAddMonoid`, `addRightMono`, `le_iff_of_unique`, `total_le`, `DFinsupp.toColex_monotone`, `isOrderedAddMonoid`, `addLeftMono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftMono` 📖	mathematical	`AddLeftStrictMono` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AddLeftMono` `Colex` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddColex` `DFinsupp.instAdd` `Preorder.toLE` `partialOrder`	—	`DFinsupp.Lex.addLeftMono`
`addLeftStrictMono` 📖	mathematical	`AddLeftStrictMono` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Colex` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddColex` `DFinsupp.instAdd` `DFinsupp.instLTColex`	—	`DFinsupp.Lex.addLeftStrictMono`
`addRightMono` 📖	mathematical	`AddRightStrictMono` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AddRightMono` `Colex` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddColex` `DFinsupp.instAdd` `Preorder.toLE` `partialOrder`	—	`DFinsupp.Lex.addRightMono`
`addRightStrictMono` 📖	mathematical	`AddRightStrictMono` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Colex` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddColex` `DFinsupp.instAdd` `DFinsupp.instLTColex`	—	`DFinsupp.Lex.addRightStrictMono`
`isOrderedAddMonoid` 📖	mathematical	`IsOrderedAddMonoid` `AddCommGroup.toAddCommMonoid`	`Colex` `DFinsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommMonoidColex` `DFinsupp.addCommMonoid` `partialOrder`	—	`DFinsupp.Lex.isOrderedAddMonoid`
`isOrderedCancelAddMonoid` 📖	mathematical	`IsOrderedCancelAddMonoid`	`Colex` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidColex` `DFinsupp.addCommMonoid` `partialOrder`	—	`DFinsupp.Lex.isOrderedCancelAddMonoid`
`isStrictOrder` 📖	mathematical	—	`IsStrictOrder` `Colex` `DFinsupp` `DFinsupp.instLTColex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`DFinsupp.Lex.isStrictOrder`
`le_iff_of_unique` 📖	mathematical	—	`Colex` `DFinsupp` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Unique.instInhabited` `DFunLike.coe` `DFinsupp.instDFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex`	—	`DFinsupp.Lex.le_iff_of_unique`
`lt_iff` 📖	mathematical	—	`Colex` `DFinsupp` `DFinsupp.instLTColex` `DFunLike.coe` `DFinsupp.instDFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex`	—	—
`total_le` 📖	mathematical	—	`Colex` `DFinsupp` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`DFinsupp.Lex.total_le`

DFinsupp.Lex

Definitions

Name	Category	Theorems
`decidableLE` 📖	CompOp	—
`decidableLT` 📖	CompOp	—
`linearOrder` 📖	CompOp	—
`orderBot` 📖	CompOp	—
`partialOrder` 📖	CompOp	8 math math: `DFinsupp.toLex_monotone`, `isOrderedCancelAddMonoid`, `isOrderedAddMonoid`, `le_iff_of_unique`, `addRightMono`, `DFinsupp.lex_le_iff_of_unique`, `addLeftMono`, `total_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addLeftMono` 📖	mathematical	`AddLeftStrictMono` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AddLeftMono` `Lex` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddLex` `DFinsupp.instAdd` `Preorder.toLE` `partialOrder`	—	`addLeftMono_of_addLeftStrictMono` `addLeftStrictMono`
`addLeftStrictMono` 📖	mathematical	`AddLeftStrictMono` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Lex` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddLex` `DFinsupp.instAdd` `DFinsupp.instLTLex`	—	`add_lt_add_right`
`addRightMono` 📖	mathematical	`AddRightStrictMono` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`AddRightMono` `Lex` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddLex` `DFinsupp.instAdd` `Preorder.toLE` `partialOrder`	—	`addRightMono_of_addRightStrictMono` `addRightStrictMono`
`addRightStrictMono` 📖	mathematical	`AddRightStrictMono` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Lex` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddLex` `DFinsupp.instAdd` `DFinsupp.instLTLex`	—	`add_lt_add_left`
`isOrderedAddMonoid` 📖	mathematical	`IsOrderedAddMonoid` `AddCommGroup.toAddCommMonoid`	`Lex` `DFinsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommMonoidLex` `DFinsupp.addCommMonoid` `partialOrder`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `isOrderedCancelAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`
`isOrderedCancelAddMonoid` 📖	mathematical	`IsOrderedCancelAddMonoid`	`Lex` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidLex` `DFinsupp.addCommMonoid` `partialOrder`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `Pi.Lex.isOrderedAddCancelMonoid` `le_of_add_le_add_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddLex` `Pi.instIsLeftCancelAdd` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsOrderedCancelAddMonoid.toAddLeftReflectLT`
`isStrictOrder` 📖	mathematical	—	`IsStrictOrder` `Lex` `DFinsupp` `DFinsupp.instLTLex` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`lt_irrefl` `lt_trans`
`le_iff_of_unique` 📖	mathematical	—	`Lex` `DFinsupp` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `Unique.instInhabited` `DFunLike.coe` `DFinsupp.instDFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`Pi.lex_le_iff_of_unique`
`lt_iff` 📖	mathematical	—	`Lex` `DFinsupp` `DFinsupp.instLTLex` `DFunLike.coe` `DFinsupp.instDFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`lt_iff_of_unique` 📖	mathematical	—	`Lex` `DFinsupp` `DFinsupp.instLTLex` `Preorder.toLT` `Unique.instInhabited` `DFunLike.coe` `DFinsupp.instDFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`DFinsupp.lex_iff_of_unique` `instIrreflLt`
`total_le` 📖	mathematical	—	`Lex` `DFinsupp` `Preorder.toLE` `PartialOrder.toPreorder` `partialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`LT.lt.le` `Eq.le`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lex_eq_dfinsupp_lex` 📖	mathematical	—	`Lex` `DFunLike.coe` `DFinsupp` `DFinsupp.instDFunLike` `DFinsupp.Lex`	—	—

---

← Back to Index