PiLex

Statistics

Metric	Count
Definitions `linearOrder`, `linearOrder`, `instBoundedOrderColexForallOfWellFoundedGT`, `instBoundedOrderLexForallOfWellFoundedLT`, `instLTColexForall`, `instLTLexForall`, `instOrderBotColexForallOfWellFoundedGT`, `instOrderBotLexForallOfWellFoundedLT`, `instOrderTopColexForallOfWellFoundedGT`, `instOrderTopLexForallOfWellFoundedLT`, `instPartialOrderColexForallOfLinearOrder`, `instPartialOrderLexForallOfLinearOrder`, `«termΠₗ_,_»`	13
Theorems `isStrictOrder`, `lt_iff_of_unique`, `noMaxOrder'`, `isStrictOrder`, `lt_iff_of_unique`, `noMaxOrder'`, `apply_le_of_toColex`, `apply_le_of_toLex`, `colex_asc`, `colex_le_iff_of_unique`, `colex_lt_iff_of_unique`, `instDenselyOrderedColexForall`, `instDenselyOrderedLexForall`, `instNoMaxOrderColexForallOfWellFoundedGTOfNonempty`, `instNoMaxOrderLexForallOfWellFoundedLTOfNonempty`, `instNoMinOrderColexForallOfWellFoundedGTOfNonempty`, `instNoMinOrderLexForallOfWellFoundedLTOfNonempty`, `isTrichotomous_lex`, `le_toColex_update_self_iff`, `le_toLex_update_self_iff`, `lex_desc`, `lex_iff_of_unique`, `lex_le_iff_of_unique`, `lex_lt_iff_of_unique`, `lex_lt_of_lt`, `lex_lt_of_lt_of_preorder`, `lt_toColex_update_self_iff`, `lt_toLex_update_self_iff`, `ofColex_apply`, `ofLex_apply`, `toColex_apply`, `toColex_monotone`, `toColex_strictMono`, `toColex_update_le_self_iff`, `toColex_update_lt_self_iff`, `toLex_apply`, `toLex_monotone`, `toLex_strictMono`, `toLex_update_le_self_iff`, `toLex_update_lt_self_iff`, `trichotomous_lex`	41
Total	54

Pi

Definitions

Name	Category	Theorems
`instBoundedOrderColexForallOfWellFoundedGT` 📖	CompOp	—
`instBoundedOrderLexForallOfWellFoundedLT` 📖	CompOp	—
`instLTColexForall` 📖	CompOp	11 math math: `colex_asc`, `Colex.lt_iff_of_unique`, `Colex.noMaxOrder'`, `Colex.isStrictOrder`, `lt_toColex_update_self_iff`, `instDenselyOrderedColexForall`, `Colex.wellFoundedLT`, `instNoMaxOrderColexForallOfWellFoundedGTOfNonempty`, `instNoMinOrderColexForallOfWellFoundedGTOfNonempty`, `colex_lt_iff_of_unique`, `toColex_update_lt_self_iff`
`instLTLexForall` 📖	CompOp	12 math math: `instNoMinOrderLexForallOfWellFoundedLTOfNonempty`, `toLex_update_lt_self_iff`, `Function.Lex.wellFoundedLT`, `lex_desc`, `lex_lt_iff_of_unique`, `Lex.wellFoundedLT`, `Lex.lt_iff_of_unique`, `lt_toLex_update_self_iff`, `instDenselyOrderedLexForall`, `instNoMaxOrderLexForallOfWellFoundedLTOfNonempty`, `Lex.isStrictOrder`, `Lex.noMaxOrder'`
`instOrderBotColexForallOfWellFoundedGT` 📖	CompOp	—
`instOrderBotLexForallOfWellFoundedLT` 📖	CompOp	—
`instOrderTopColexForallOfWellFoundedGT` 📖	CompOp	—
`instOrderTopLexForallOfWellFoundedLT` 📖	CompOp	—
`instPartialOrderColexForallOfLinearOrder` 📖	CompOp	5 math math: `toColex_monotone`, `colex_le_iff_of_unique`, `toColex_strictMono`, `toColex_update_le_self_iff`, `le_toColex_update_self_iff`
`instPartialOrderLexForallOfLinearOrder` 📖	CompOp	7 math math: `lex_le_iff_of_unique`, `toLex_update_le_self_iff`, `le_toLex_update_self_iff`, `Lex.isOrderedAddCancelMonoid`, `Lex.isOrderedCancelMonoid`, `toLex_strictMono`, `toLex_monotone`
`«termΠₗ_,_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_le_of_toColex` 📖	—	`Colex` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderColexForallOfLinearOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `not_le_of_gt`
`apply_le_of_toLex` 📖	—	`Lex` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderLexForallOfLinearOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `not_le_of_gt`
`colex_asc` 📖	mathematical	`Preorder.toLE`	`Colex` `instLTColexForall` `Preorder.toLT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Equiv.Perm` `Equiv.swap`	—	`Equiv.swap_comm` `lex_desc`
`colex_le_iff_of_unique` 📖	mathematical	—	`Colex` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderColexForallOfLinearOrder` `Unique.instInhabited`	—	—
`colex_lt_iff_of_unique` 📖	mathematical	—	`Colex` `instLTColexForall` `Preorder.toLT` `Unique.instInhabited`	—	`Colex.lt_iff_of_unique`
`instDenselyOrderedColexForall` 📖	mathematical	`DenselyOrdered`	`Colex` `instLTColexForall` `Preorder.toLT`	—	`instDenselyOrderedLexForall`
`instDenselyOrderedLexForall` 📖	mathematical	`DenselyOrdered`	`Lex` `instLTLexForall` `Preorder.toLT`	—	`exists_between` `Function.update_of_ne` `LT.lt.ne` `Function.update_self`
`instNoMaxOrderColexForallOfWellFoundedGTOfNonempty` 📖	mathematical	`NoMaxOrder` `Preorder.toLT` `PartialOrder.toPreorder`	`Colex` `instLTColexForall` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`instNoMaxOrderLexForallOfWellFoundedLTOfNonempty` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT` `OrderDual.instNonempty`
`instNoMaxOrderLexForallOfWellFoundedLTOfNonempty` 📖	mathematical	`NoMaxOrder` `Preorder.toLT` `PartialOrder.toPreorder`	`Lex` `instLTLexForall` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`NoMaxOrder.exists_gt` `instNoMaxOrderForallOfNonempty` `toLex_strictMono`
`instNoMinOrderColexForallOfWellFoundedGTOfNonempty` 📖	mathematical	`NoMinOrder` `Preorder.toLT` `PartialOrder.toPreorder`	`Colex` `instLTColexForall` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`instNoMinOrderLexForallOfWellFoundedLTOfNonempty` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT` `OrderDual.instNonempty`
`instNoMinOrderLexForallOfWellFoundedLTOfNonempty` 📖	mathematical	`NoMinOrder` `Preorder.toLT` `PartialOrder.toPreorder`	`Lex` `instLTLexForall` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`NoMinOrder.exists_lt` `instNoMinOrderForallOfNonempty` `toLex_strictMono`
`isTrichotomous_lex` 📖	mathematical	—	`Lex`	—	`trichotomous_lex`
`le_toColex_update_self_iff` 📖	mathematical	—	`Colex` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderColexForallOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Function.update` `LinearOrder.toDecidableEq`	—	`le_toLex_update_self_iff` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT`
`le_toLex_update_self_iff` 📖	mathematical	—	`Lex` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderLexForallOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Function.update` `LinearOrder.toDecidableEq`	—	—
`lex_desc` 📖	mathematical	`Preorder.toLE`	`Lex` `instLTLexForall` `Preorder.toLT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Equiv.Perm` `Equiv.swap`	—	`Equiv.swap_apply_of_ne_of_ne` `LT.lt.ne` `LT.lt.trans_le` `Equiv.swap_apply_left`
`lex_iff_of_unique` 📖	mathematical	—	`Lex` `Unique.instInhabited`	—	`instIsEmptyFalse`
`lex_le_iff_of_unique` 📖	mathematical	—	`Lex` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderLexForallOfLinearOrder` `Unique.instInhabited`	—	—
`lex_lt_iff_of_unique` 📖	mathematical	—	`Lex` `instLTLexForall` `Preorder.toLT` `Unique.instInhabited`	—	`Lex.lt_iff_of_unique`
`lex_lt_of_lt` 📖	mathematical	`Preorder.toLT` `preorder` `PartialOrder.toPreorder`	`Lex`	—	`lex_lt_of_lt_of_preorder`
`lex_lt_of_lt_of_preorder` 📖	mathematical	`Preorder.toLT` `preorder`	`Preorder.toLE`	—	`lt_def` `WellFounded.has_min` `lt_of_le_not_ge`
`lt_toColex_update_self_iff` 📖	mathematical	—	`Colex` `instLTColexForall` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Function.update` `LinearOrder.toDecidableEq`	—	`lt_toLex_update_self_iff` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT`
`lt_toLex_update_self_iff` 📖	mathematical	—	`Lex` `instLTLexForall` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Function.update` `LinearOrder.toDecidableEq`	—	`Function.update_self` `LT.lt.false` `Function.update_of_ne` `toLex_strictMono` `lt_update_self_iff`
`ofColex_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Colex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofColex`	—	—
`ofLex_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`toColex_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Colex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	—
`toColex_monotone` 📖	mathematical	—	`Monotone` `Colex` `preorder` `PartialOrder.toPreorder` `instPartialOrderColexForallOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	`toLex_monotone` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT`
`toColex_strictMono` 📖	mathematical	—	`StrictMono` `Colex` `preorder` `PartialOrder.toPreorder` `instPartialOrderColexForallOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex`	—	`toLex_strictMono` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT`
`toColex_update_le_self_iff` 📖	mathematical	—	`Colex` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderColexForallOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Function.update` `LinearOrder.toDecidableEq`	—	`toLex_update_le_self_iff` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT`
`toColex_update_lt_self_iff` 📖	mathematical	—	`Colex` `instLTColexForall` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toColex` `Function.update` `LinearOrder.toDecidableEq`	—	`toLex_update_lt_self_iff` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT`
`toLex_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`toLex_monotone` 📖	mathematical	—	`Monotone` `Lex` `preorder` `PartialOrder.toPreorder` `instPartialOrderLexForallOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`WellFounded.has_min` `IsWellFounded.wf` `Function.ne_iff` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `LE.le.lt_of_ne`
`toLex_strictMono` 📖	mathematical	—	`StrictMono` `Lex` `preorder` `PartialOrder.toPreorder` `instPartialOrderLexForallOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`WellFounded.has_min` `IsWellFounded.wf` `Function.ne_iff` `LT.lt.ne` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `LE.le.lt_of_ne` `LT.lt.le`
`toLex_update_le_self_iff` 📖	mathematical	—	`Lex` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderLexForallOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Function.update` `LinearOrder.toDecidableEq`	—	—
`toLex_update_lt_self_iff` 📖	mathematical	—	`Lex` `instLTLexForall` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Function.update` `LinearOrder.toDecidableEq`	—	`Function.update_self` `LT.lt.false` `Function.update_of_ne` `toLex_strictMono` `update_lt_self_iff`
`trichotomous_lex` 📖	mathematical	—	`Lex`	—	`Function.ne_iff` `WellFounded.not_lt_min` `Not.imp_symm` `WellFounded.min_mem`

Pi.Colex

Definitions

Name	Category	Theorems
`linearOrder` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isStrictOrder` 📖	mathematical	—	`IsStrictOrder` `Colex` `Pi.instLTColexForall` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Pi.Lex.isStrictOrder`
`lt_iff_of_unique` 📖	mathematical	—	`Colex` `Pi.instLTColexForall` `Preorder.toLT` `Unique.instInhabited`	—	`Pi.lex_iff_of_unique` `instIrreflGt`
`noMaxOrder'` 📖	mathematical	—	`NoMaxOrder` `Colex` `Pi.instLTColexForall` `Preorder.toLT`	—	`Pi.Lex.noMaxOrder'`

Pi.Lex

Definitions

Name	Category	Theorems
`linearOrder` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isStrictOrder` 📖	mathematical	—	`IsStrictOrder` `Lex` `Pi.instLTLexForall` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`lt_irrefl` `lt_trichotomy` `LT.lt.trans`
`lt_iff_of_unique` 📖	mathematical	—	`Lex` `Pi.instLTLexForall` `Preorder.toLT` `Unique.instInhabited`	—	`Pi.lex_iff_of_unique` `instIrreflLt`
`noMaxOrder'` 📖	mathematical	—	`NoMaxOrder` `Lex` `Pi.instLTLexForall` `Preorder.toLT`	—	`NoMaxOrder.exists_gt` `Function.update_of_ne` `LT.lt.ne` `Function.update_self`

---

← Back to Index