Lex

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

Statistics

Metric	Count
Definitions `boundedOrder`, `instLE`, `instLT`, `instLinearOrder`, `instOrdLexProd`, `instPartialOrder`, `instPreorder`, `instWellFoundedRelationLexOfWellFoundedLT`, `orderBot`, `orderTop`, `«term_×ₗ_»`	11
Theorems `lex_eq`, `compare_def`, `covBy_iff`, `instDenselyOrderedLex`, `instOrientedOrdLex`, `instTransOrdLex`, `instWellFoundedLTLex`, `le_iff`, `le_iff'`, `lt_iff`, `lt_iff'`, `monotone_fst`, `monotone_fst_ofLex`, `noMaxOrder_of_left`, `noMaxOrder_of_right`, `noMinOrder_of_left`, `noMinOrder_of_right`, `toLex_covBy_toLex_iff`, `toLex_le_toLex`, `toLex_le_toLex'`, `toLex_lt_toLex`, `toLex_lt_toLex'`, `toLex_mono`, `toLex_strictMono`, `fst_ofLex`, `lexOrd_eq`	26
Total	37

Ord

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lex_eq` 📖	mathematical	—	`Prod.Lex.instOrdLexProd`	—	—

Prod.Lex

Definitions

Name	Category	Theorems
`boundedOrder` 📖	CompOp	—
`instLE` 📖	CompOp	15 math math: `toLex_le_toLex'`, `prodLexAssoc_symm_apply`, `sumLexProdLexDistrib_symm_apply`, `Tuple.graphEquiv₂_apply`, `le_iff`, `Tuple.self_comp_sort`, `sumLexProdLexDistrib_apply`, `uniqueProd_apply`, `HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd`, `HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst`, `prodUnique_apply`, `toLex_le_toLex`, `prodLexCongr_apply`, `prodLexAssoc_apply`, `le_iff'`
`instLT` 📖	CompOp	15 math math: `toLex_lt_toLex'`, `lt_iff'`, `instDenselyOrderedLex`, `prodLexAssoc_symm_apply`, `noMaxOrder_of_left`, `noMinOrder_of_left`, `toLex_lt_toLex`, `covBy_iff`, `noMinOrder_of_right`, `noMaxOrder_of_right`, `toLex_covBy_toLex_iff`, `instWellFoundedLTLex`, `lt_iff`, `Finsupp.DegLex.lt_def`, `prodLexAssoc_apply`
`instLinearOrder` 📖	CompOp	4 math math: `OrderType.type_lex_prod`, `Finset.intervalGapsWithin_snd_of_lt`, `Finset.intervalGapsWithin_succ_fst_of_lt`, `Finset.intervalGapsWithin_fst_of_lt_lt`
`instOrdLexProd` 📖	CompOp	5 math math: `compare_def`, `instOrientedOrdLex`, `Ord.lex_eq`, `lexOrd_eq`, `instTransOrdLex`
`instPartialOrder` 📖	CompOp	8 math math: `isOrderedAddMonoid`, `HahnSeries.iterateEquiv_apply`, `isOrderedCancelMonoid`, `HVertexOperator.coeff_comp`, `isOrderedMonoid`, `HVertexOperator.comp_apply`, `HahnSeries.iterateEquiv_symm_apply`, `isOrderedAddCancelMonoid`
`instPreorder` 📖	CompOp	27 math math: `Set.PartiallyWellOrderedOn.subsetProdLex`, `LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex`, `monotone_fst_ofLex`, `toLexOrderHom_coe`, `OrderAddMonoidHom.addCommute_inlₗ_inrₗ`, `Tuple.monotone_proj`, `OrderMonoidHom.inrₗ_apply`, `OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex`, `OrderAddMonoidHom.fstₗ_comp_inlₗ`, `LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ`, `OrderMonoidHom.inlₗ_apply`, `OrderAddMonoidHom.inlₗ_apply`, `OrderMonoidHom.fstₗ_apply`, `LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ`, `OrderMonoidHom.commute_inlₗ_inrₗ`, `LinearOrderedCommGroupWithZero.fst_comp_inl`, `OrderAddMonoidHom.inlₗ_add_inrₗ_eq_toLex`, `toLex_mono`, `LinearOrderedCommGroupWithZero.fst_apply`, `Tuple.eq_sort_iff'`, `OrderAddMonoidHom.fstₗ_apply`, `toLex_strictMono`, `OrderMonoidHom.fstₗ_comp_inlₗ`, `LinearOrderedCommGroupWithZero.inl_apply`, `LinearOrderedCommGroupWithZero.inr_apply`, `OrderAddMonoidHom.inrₗ_apply`, `Set.PartiallyWellOrderedOn.ProdLex_iff`
`instWellFoundedRelationLexOfWellFoundedLT` 📖	CompOp	—
`orderBot` 📖	CompOp	—
`orderTop` 📖	CompOp	—
`«term_×ₗ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compare_def` 📖	mathematical	—	`Lex` `instOrdLexProd` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`covBy_iff` 📖	mathematical	—	`CovBy` `Lex` `instLT` `Preorder.toLT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `IsMax` `Preorder.toLE` `IsMin`	—	`toLex_covBy_toLex_iff`
`instDenselyOrderedLex` 📖	mathematical	—	`DenselyOrdered` `Lex` `instLT` `Preorder.toLT`	—	`exists_between`
`instOrientedOrdLex` 📖	mathematical	—	`Lex` `instOrdLexProd`	—	—
`instTransOrdLex` 📖	mathematical	—	`Lex` `instOrdLexProd`	—	—
`instWellFoundedLTLex` 📖	mathematical	—	`WellFoundedLT` `Lex` `instLT`	—	`instIsWellFounded`
`le_iff` 📖	mathematical	—	`Lex` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`le_iff'` 📖	mathematical	—	`Lex` `instLE` `Preorder.toLT` `PartialOrder.toPreorder` `Preorder.toLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`toLex_le_toLex'`
`lt_iff` 📖	mathematical	—	`Lex` `instLT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`lt_iff'` 📖	mathematical	—	`Lex` `instLT` `Preorder.toLT` `PartialOrder.toPreorder` `Preorder.toLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`toLex_lt_toLex'`
`monotone_fst` 📖	mathematical	`Lex` `instLE` `Preorder.toLT`	`Preorder.toLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`toLex_le_toLex` `LT.lt.le` `Eq.le`
`monotone_fst_ofLex` 📖	mathematical	—	`Monotone` `Lex` `instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`monotone_fst`
`noMaxOrder_of_left` 📖	mathematical	—	`NoMaxOrder` `Lex` `instLT` `Preorder.toLT`	—	`NoMaxOrder.exists_gt`
`noMaxOrder_of_right` 📖	mathematical	—	`NoMaxOrder` `Lex` `instLT` `Preorder.toLT`	—	`NoMaxOrder.exists_gt`
`noMinOrder_of_left` 📖	mathematical	—	`NoMinOrder` `Lex` `instLT` `Preorder.toLT`	—	`NoMinOrder.exists_lt`
`noMinOrder_of_right` 📖	mathematical	—	`NoMinOrder` `Lex` `instLT` `Preorder.toLT`	—	`NoMinOrder.exists_lt`
`toLex_covBy_toLex_iff` 📖	mathematical	—	`CovBy` `Lex` `instLT` `Preorder.toLT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `IsMax` `Preorder.toLE` `IsMin`	—	`Function.Surjective.forall` `Equiv.surjective`
`toLex_le_toLex` 📖	mathematical	—	`Lex` `instLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`toLex_le_toLex'` 📖	mathematical	—	`Lex` `instLE` `Preorder.toLT` `PartialOrder.toPreorder` `Preorder.toLE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`toLex_lt_toLex` 📖	mathematical	—	`Lex` `instLT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`toLex_lt_toLex'` 📖	mathematical	—	`Lex` `instLT` `Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Preorder.toLE`	—	`toLex_lt_toLex`
`toLex_mono` 📖	mathematical	—	`Monotone` `Lex` `Prod.instPreorder` `PartialOrder.toPreorder` `instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`toLex_le_toLex'`
`toLex_strictMono` 📖	mathematical	—	`StrictMono` `Lex` `Prod.instPreorder` `PartialOrder.toPreorder` `instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`LE.le.eq_or_lt` `LT.lt.le` `Prod.mk_lt_mk_iff_right`

WCovBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_ofLex` 📖	mathematical	`WCovBy` `Lex` `Prod.Lex.instPreorder`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	`Prod.Lex.monotone_fst`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lexOrd_eq` 📖	mathematical	—	`Prod.Lex.instOrdLexProd`	—	—

---

← Back to Index