Order

📁 Source: Mathlib/Data/Sum/Order.lean

Statistics

Metric	Count
Definitions `emptySumLex`, `sumAssoc`, `sumComm`, `sumCongr`, `sumDualDistrib`, `sumLexAssoc`, `sumLexCongr`, `sumLexDualAntidistrib`, `sumLexEmpty`, `LE`, `LT`, `boundedOrder`, `linearOrder`, `orderBot`, `orderTop`, `partialOrder`, `preorder`, `toLexRelIsoLE`, `toLexRelIsoLT`, `«term_⊕ₗ_»`, `inlₗ`, `inrₗ`, `instLESum`, `instLTSum`, `instPartialOrder`, `instPreorderSum`, `orderIsoPUnitSumLex`, `orderIsoSumLexPUnit`	28
Theorems `emptySumLex_apply_inr`, `sumAssoc_apply_inl_inl`, `sumAssoc_apply_inl_inr`, `sumAssoc_apply_inr`, `sumAssoc_symm_apply_inl`, `sumAssoc_symm_apply_inr_inl`, `sumAssoc_symm_apply_inr_inr`, `sumComm_apply`, `sumComm_symm`, `sumCongr_apply`, `sumCongr_refl`, `sumCongr_symm`, `sumCongr_trans`, `sumDualDistrib_inl`, `sumDualDistrib_inr`, `sumDualDistrib_symm_inl`, `sumDualDistrib_symm_inr`, `sumLexAssoc_apply_inl_inl`, `sumLexAssoc_apply_inl_inr`, `sumLexAssoc_apply_inr`, `sumLexAssoc_symm_apply_inl`, `sumLexAssoc_symm_apply_inr_inl`, `sumLexAssoc_symm_apply_inr_inr`, `sumLexCongr_apply`, `sumLexCongr_refl`, `sumLexCongr_symm`, `sumLexCongr_trans`, `sumLexDualAntidistrib_inl`, `sumLexDualAntidistrib_inr`, `sumLexDualAntidistrib_symm_inl`, `sumLexDualAntidistrib_symm_inr`, `sumLexEmpty_apply_inl`, `denselyOrdered_of_noMaxOrder`, `denselyOrdered_of_noMinOrder`, `inl_bot`, `inl_le_inl_iff`, `inl_le_inr`, `inl_lt_inl_iff`, `inl_lt_inr`, `inl_mono`, `inl_strictMono`, `inr_le_inr_iff`, `inr_lt_inr_iff`, `inr_mono`, `inr_strictMono`, `inr_top`, `le_def`, `lt_def`, `noMaxOrder`, `noMaxOrder_of_nonempty`, `noMinOrder`, `noMinOrder_of_nonempty`, `not_inr_le_inl`, `not_inr_lt_inl`, `toLexRelIsoLE_coe`, `toLexRelIsoLE_symm_coe`, `toLexRelIsoLT_coe`, `toLexRelIsoLT_symm_coe`, `toLex_le_toLex`, `toLex_lt_toLex`, `toLex_mono`, `toLex_strictMono`, `refl`, `trans`, `denselyOrdered`, `denselyOrdered_iff`, `inl_le_inl_iff`, `inl_lt_inl_iff`, `inl_mono`, `inl_strictMono`, `inr_le_inr_iff`, `inr_lt_inr_iff`, `inr_mono`, `inr_strictMono`, `instAntisymmLex_mathlib`, `instAntisymmLiftRel_mathlib`, `instIrreflLex_mathlib`, `instIrreflLiftRel_mathlib`, `instIsTransLex`, `instIsTransLiftRel`, `instIsWellOrderLex`, `instReflLex_mathlib`, `instReflLiftRel_mathlib`, `instTotalLex_mathlib`, `instTrichotomousLex_mathlib`, `le_def`, `lt_def`, `noMaxOrder`, `noMaxOrder_iff`, `noMinOrder`, `noMinOrder_iff`, `not_inl_le_inr`, `not_inl_lt_inr`, `not_inr_le_inl`, `not_inr_lt_inl`, `swap_le_swap_iff`, `swap_lt_swap_iff`, `orderIsoPUnitSumLex_bot`, `orderIsoPUnitSumLex_symm_inl`, `orderIsoPUnitSumLex_symm_inr`, `orderIsoPUnitSumLex_toLex`, `orderIsoSumLexPUnit_symm_inl`, `orderIsoSumLexPUnit_symm_inr`, `orderIsoSumLexPUnit_toLex`, `orderIsoSumLexPUnit_top`	105
Total	133

OrderIso

Definitions

Name	Category	Theorems
`emptySumLex` 📖	CompOp	1 math math: `emptySumLex_apply_inr`
`sumAssoc` 📖	CompOp	6 math math: `sumAssoc_apply_inl_inl`, `sumAssoc_apply_inr`, `sumAssoc_symm_apply_inr_inl`, `sumAssoc_symm_apply_inr_inr`, `sumAssoc_apply_inl_inr`, `sumAssoc_symm_apply_inl`
`sumComm` 📖	CompOp	2 math math: `sumComm_symm`, `sumComm_apply`
`sumCongr` 📖	CompOp	4 math math: `sumCongr_apply`, `sumCongr_symm`, `sumCongr_trans`, `sumCongr_refl`
`sumDualDistrib` 📖	CompOp	4 math math: `sumDualDistrib_symm_inl`, `sumDualDistrib_inl`, `sumDualDistrib_symm_inr`, `sumDualDistrib_inr`
`sumLexAssoc` 📖	CompOp	6 math math: `sumLexAssoc_symm_apply_inr_inr`, `sumLexAssoc_symm_apply_inr_inl`, `sumLexAssoc_apply_inl_inl`, `sumLexAssoc_apply_inr`, `sumLexAssoc_symm_apply_inl`, `sumLexAssoc_apply_inl_inr`
`sumLexCongr` 📖	CompOp	4 math math: `sumLexCongr_trans`, `sumLexCongr_apply`, `sumLexCongr_refl`, `sumLexCongr_symm`
`sumLexDualAntidistrib` 📖	CompOp	4 math math: `sumLexDualAntidistrib_symm_inl`, `sumLexDualAntidistrib_symm_inr`, `sumLexDualAntidistrib_inr`, `sumLexDualAntidistrib_inl`
`sumLexEmpty` 📖	CompOp	1 math math: `sumLexEmpty_apply_inl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`emptySumLex_apply_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Sum.Lex.LE` `instFunLikeOrderIso` `emptySumLex` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`sumAssoc_apply_inl_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Sum.instLESum` `instFunLikeOrderIso` `sumAssoc`	—	—
`sumAssoc_apply_inl_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Sum.instLESum` `instFunLikeOrderIso` `sumAssoc`	—	—
`sumAssoc_apply_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Sum.instLESum` `instFunLikeOrderIso` `sumAssoc`	—	—
`sumAssoc_symm_apply_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Sum.instLESum` `instFunLikeOrderIso` `symm` `sumAssoc`	—	—
`sumAssoc_symm_apply_inr_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Sum.instLESum` `instFunLikeOrderIso` `symm` `sumAssoc`	—	—
`sumAssoc_symm_apply_inr_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Sum.instLESum` `instFunLikeOrderIso` `symm` `sumAssoc`	—	—
`sumComm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Sum.instLESum` `RelIso.instFunLike` `sumComm`	—	—
`sumComm_symm` 📖	mathematical	—	`symm` `Sum.instLESum` `sumComm`	—	—
`sumCongr_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Sum.instLESum` `RelIso.instFunLike` `sumCongr` `OrderIso` `EquivLike.toFunLike` `instEquivLike`	—	—
`sumCongr_refl` 📖	mathematical	—	`sumCongr` `refl` `Sum.instLESum`	—	`ext`
`sumCongr_symm` 📖	mathematical	—	`symm` `Sum.instLESum` `sumCongr`	—	—
`sumCongr_trans` 📖	mathematical	—	`trans` `Sum.instLESum` `sumCongr`	—	`ext`
`sumDualDistrib_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `OrderDual.instLE` `Sum.instLESum` `instFunLikeOrderIso` `sumDualDistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`sumDualDistrib_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `OrderDual.instLE` `Sum.instLESum` `instFunLikeOrderIso` `sumDualDistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`sumDualDistrib_symm_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `Sum.instLESum` `OrderDual.instLE` `instFunLikeOrderIso` `symm` `sumDualDistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`sumDualDistrib_symm_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `Sum.instLESum` `OrderDual.instLE` `instFunLikeOrderIso` `symm` `sumDualDistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`sumLexAssoc_apply_inl_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Sum.Lex.LE` `instFunLikeOrderIso` `sumLexAssoc` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`sumLexAssoc_apply_inl_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Sum.Lex.LE` `instFunLikeOrderIso` `sumLexAssoc` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`sumLexAssoc_apply_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Sum.Lex.LE` `instFunLikeOrderIso` `sumLexAssoc` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`sumLexAssoc_symm_apply_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Sum.Lex.LE` `instFunLikeOrderIso` `symm` `sumLexAssoc`	—	—
`sumLexAssoc_symm_apply_inr_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Sum.Lex.LE` `instFunLikeOrderIso` `symm` `sumLexAssoc`	—	—
`sumLexAssoc_symm_apply_inr_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Sum.Lex.LE` `instFunLikeOrderIso` `symm` `sumLexAssoc`	—	—
`sumLexCongr_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Lex` `Sum.Lex.LE` `RelIso.instFunLike` `sumLexCongr` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `OrderIso` `instEquivLike` `ofLex`	—	—
`sumLexCongr_refl` 📖	mathematical	—	`sumLexCongr` `refl` `Lex` `Sum.Lex.LE`	—	`ext`
`sumLexCongr_symm` 📖	mathematical	—	`symm` `Lex` `Sum.Lex.LE` `sumLexCongr`	—	—
`sumLexCongr_trans` 📖	mathematical	—	`trans` `Lex` `Sum.Lex.LE` `sumLexCongr`	—	`ext`
`sumLexDualAntidistrib_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `Lex` `OrderDual.instLE` `Sum.Lex.LE` `instFunLikeOrderIso` `sumLexDualAntidistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`sumLexDualAntidistrib_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `Lex` `OrderDual.instLE` `Sum.Lex.LE` `instFunLikeOrderIso` `sumLexDualAntidistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`sumLexDualAntidistrib_symm_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `OrderDual` `Sum.Lex.LE` `OrderDual.instLE` `instFunLikeOrderIso` `symm` `sumLexDualAntidistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`sumLexDualAntidistrib_symm_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `OrderDual` `Sum.Lex.LE` `OrderDual.instLE` `instFunLikeOrderIso` `symm` `sumLexDualAntidistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`sumLexEmpty_apply_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `Sum.Lex.LE` `instFunLikeOrderIso` `sumLexEmpty` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—

Sum

Definitions

Name	Category	Theorems
`inlₗ` 📖	CompOp	18 math math: `Lex.Ico_inl_inl`, `Lex.Ioo_inl_inr`, `Lex.Ioo_inr_inl`, `Lex.Icc_inl_inl`, `Lex.Ici_inl`, `Lex.Ioc_inl_inl`, `Lex.Icc_inr_inl`, `Lex.Ioc_inl_inr`, `Lex.Iio_inl`, `Lex.Ioc_inr_inl`, `Lex.Ioi_inl`, `Lex.Ioo_inl_inl`, `Lex.Iic_inl`, `Lex.Ico_inr_inl`, `Lex.Ico_inl_inr`, `Lex.inl_inf`, `Lex.Icc_inl_inr`, `Lex.inl_sup`
`inrₗ` 📖	CompOp	18 math math: `Lex.Icc_inr_inr`, `Lex.Ico_inr_inr`, `Lex.Ioo_inl_inr`, `Lex.Ioo_inr_inl`, `Lex.Iic_inr`, `Lex.Ioo_inr_inr`, `Lex.Ioi_inr`, `Lex.Icc_inr_inl`, `Lex.Ioc_inl_inr`, `Lex.Ioc_inr_inl`, `Lex.inr_inf`, `Lex.Ioc_inr_inr`, `Lex.Ici_inr`, `Lex.Ico_inr_inl`, `Lex.Ico_inl_inr`, `Lex.Iio_inr`, `Lex.inr_sup`, `Lex.Icc_inl_inr`
`instLESum` 📖	CompOp	22 math math: `OrderIso.sumAssoc_apply_inl_inl`, `OrderIso.sumCongr_apply`, `OrderIso.sumCongr_symm`, `inr_le_inr_iff`, `OrderIso.sumComm_symm`, `OrderIso.sumDualDistrib_symm_inl`, `OrderIso.sumAssoc_apply_inr`, `le_def`, `not_inr_le_inl`, `OrderIso.sumAssoc_symm_apply_inr_inl`, `OrderIso.sumCongr_trans`, `OrderIso.sumComm_apply`, `OrderIso.sumDualDistrib_inl`, `OrderIso.sumDualDistrib_symm_inr`, `OrderIso.sumAssoc_symm_apply_inr_inr`, `OrderIso.sumDualDistrib_inr`, `inl_le_inl_iff`, `swap_le_swap_iff`, `OrderIso.sumAssoc_apply_inl_inr`, `OrderIso.sumAssoc_symm_apply_inl`, `OrderIso.sumCongr_refl`, `not_inl_le_inr`
`instLTSum` 📖	CompOp	12 math math: `noMinOrder`, `lt_def`, `swap_lt_swap_iff`, `denselyOrdered`, `inr_lt_inr_iff`, `not_inr_lt_inl`, `noMinOrder_iff`, `noMaxOrder`, `noMaxOrder_iff`, `denselyOrdered_iff`, `not_inl_lt_inr`, `inl_lt_inl_iff`
`instPartialOrder` 📖	CompOp	—
`instPreorderSum` 📖	CompOp	30 math math: `Ico_inl_inl`, `Iio_inr`, `Ioc_inl_inr`, `Ici_inr`, `Ioo_inl_inr`, `Icc_inr_inr`, `Ioc_inr_inr`, `Ioi_inr`, `Iio_inl`, `Ioo_inr_inr`, `inl_strictMono`, `inl_mono`, `Ioo_inr_inl`, `Icc_inl_inr`, `Ioo_inl_inl`, `Ici_inl`, `Iic_inl`, `Ico_inr_inr`, `Icc_inr_inl`, `Iic_inr`, `Ico_inl_inr`, `inr_strictMono`, `Ioi_inl`, `Lex.toLex_strictMono`, `Ioc_inr_inl`, `Ioc_inl_inl`, `inr_mono`, `Lex.toLex_mono`, `Ico_inr_inl`, `Icc_inl_inl`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`denselyOrdered` 📖	mathematical	—	`DenselyOrdered` `instLTSum`	—	`exists_between`
`denselyOrdered_iff` 📖	mathematical	—	`DenselyOrdered` `instLTSum`	—	`exists_between` `inl_lt_inl_iff` `not_inl_lt_inr` `inr_lt_inr_iff` `denselyOrdered`
`inl_le_inl_iff` 📖	mathematical	—	`instLESum`	—	—
`inl_lt_inl_iff` 📖	mathematical	—	`instLTSum`	—	—
`inl_mono` 📖	mathematical	—	`Monotone` `instPreorderSum`	—	—
`inl_strictMono` 📖	mathematical	—	`StrictMono` `instPreorderSum`	—	—
`inr_le_inr_iff` 📖	mathematical	—	`instLESum`	—	—
`inr_lt_inr_iff` 📖	mathematical	—	`instLTSum`	—	—
`inr_mono` 📖	mathematical	—	`Monotone` `instPreorderSum`	—	—
`inr_strictMono` 📖	mathematical	—	`StrictMono` `instPreorderSum`	—	—
`instAntisymmLex_mathlib` 📖	—	—	—	—	`antisymm`
`instAntisymmLiftRel_mathlib` 📖	—	—	—	—	`antisymm`
`instIrreflLex_mathlib` 📖	—	—	—	—	`irrefl`
`instIrreflLiftRel_mathlib` 📖	—	—	—	—	`irrefl`
`instIsTransLex` 📖	mathematical	—	`IsTrans`	—	`trans`
`instIsTransLiftRel` 📖	mathematical	—	`IsTrans`	—	`LiftRel.trans`
`instIsWellOrderLex` 📖	mathematical	—	`IsWellOrder`	—	`instTrichotomousLex_mathlib` `IsWellOrder.toTrichotomous` `instIsTransLex` `IsWellOrder.toIsTrans` `IsWellFounded.wf` `IsWellOrder.toIsWellFounded`
`instReflLex_mathlib` 📖	—	—	—	—	`refl`
`instReflLiftRel_mathlib` 📖	—	—	—	—	`LiftRel.refl`
`instTotalLex_mathlib` 📖	—	—	—	—	`total_of`
`instTrichotomousLex_mathlib` 📖	—	—	—	—	—
`le_def` 📖	mathematical	—	`instLESum`	—	—
`lt_def` 📖	mathematical	—	`instLTSum`	—	—
`noMaxOrder` 📖	mathematical	—	`NoMaxOrder` `instLTSum`	—	`NoMaxOrder.exists_gt` `inl_lt_inl_iff` `inr_lt_inr_iff`
`noMaxOrder_iff` 📖	mathematical	—	`NoMaxOrder` `instLTSum`	—	`NoMaxOrder.exists_gt` `inl_lt_inl_iff` `not_inl_lt_inr` `not_inr_lt_inl` `inr_lt_inr_iff` `noMaxOrder`
`noMinOrder` 📖	mathematical	—	`NoMinOrder` `instLTSum`	—	`NoMinOrder.exists_lt` `inl_lt_inl_iff` `inr_lt_inr_iff`
`noMinOrder_iff` 📖	mathematical	—	`NoMinOrder` `instLTSum`	—	`NoMinOrder.exists_lt` `inl_lt_inl_iff` `not_inr_lt_inl` `not_inl_lt_inr` `inr_lt_inr_iff` `noMinOrder`
`not_inl_le_inr` 📖	mathematical	—	`instLESum`	—	—
`not_inl_lt_inr` 📖	mathematical	—	`instLTSum`	—	—
`not_inr_le_inl` 📖	mathematical	—	`instLESum`	—	—
`not_inr_lt_inl` 📖	mathematical	—	`instLTSum`	—	—
`swap_le_swap_iff` 📖	mathematical	—	`instLESum`	—	—
`swap_lt_swap_iff` 📖	mathematical	—	`instLTSum`	—	—

Sum.Lex

Definitions

Name	Category	Theorems
`LE` 📖	CompOp	48 math math: `WithBot.orderIsoPUnitSumLex_symm_inl`, `OrderIso.sumLexIicIoi_symm_apply_of_lt`, `inr_le_inr_iff`, `WithBot.orderIsoPUnitSumLex_symm_inr`, `OrderIso.sumLexIioIci_symm_apply_Ici`, `OrderIso.sumLexAssoc_symm_apply_inr_inr`, `OrderIso.sumLexCongr_trans`, `inl_bot`, `OrderIso.sumLexIicIoi_symm_apply_of_le`, `WithTop.orderIsoSumLexPUnit_toLex`, `Prod.Lex.sumLexProdLexDistrib_symm_apply`, `toLexRelIsoLE_coe`, `WithTop.orderIsoSumLexPUnit_symm_inl`, `OrderIso.sumLexIioIci_symm_apply_Iio`, `toLex_le_toLex`, `toLexRelIsoLE_symm_coe`, `OrderIso.sumLexIicIoi_symm_apply_Iic`, `Prod.Lex.sumLexProdLexDistrib_apply`, `WithTop.orderIsoSumLexPUnit_top`, `OrderIso.sumLexCongr_apply`, `OrderIso.sumLexIicIoi_symm_apply_Ioi`, `OrderIso.sumLexIicIoi_apply_inr`, `OrderIso.sumLexAssoc_symm_apply_inr_inl`, `OrderIso.sumLexAssoc_apply_inl_inl`, `OrderIso.sumLexEmpty_apply_inl`, `OrderIso.sumLexIicIoi_apply_inl`, `OrderIso.sumLexCongr_refl`, `WithBot.orderIsoPUnitSumLex_toLex`, `OrderIso.emptySumLex_apply_inr`, `OrderIso.sumLexDualAntidistrib_symm_inl`, `OrderIso.sumLexIioIci_symm_apply_of_ge`, `OrderIso.sumLexCongr_symm`, `OrderIso.sumLexIioIci_apply_inl`, `WithTop.orderIsoSumLexPUnit_symm_inr`, `OrderIso.sumLexAssoc_apply_inr`, `not_inr_le_inl`, `le_def`, `inr_top`, `OrderIso.sumLexDualAntidistrib_symm_inr`, `OrderIso.sumLexDualAntidistrib_inr`, `OrderIso.sumLexDualAntidistrib_inl`, `OrderIso.sumLexAssoc_symm_apply_inl`, `OrderIso.sumLexIioIci_apply_inr`, `OrderIso.sumLexIioIci_symm_apply_of_lt`, `OrderIso.sumLexAssoc_apply_inl_inr`, `WithBot.orderIsoPUnitSumLex_bot`, `inl_le_inr`, `inl_le_inl_iff`
`LT` 📖	CompOp	16 math math: `noMaxOrder`, `noMaxOrder_of_nonempty`, `toLex_lt_toLex`, `Prod.Lex.sumLexProdLexDistrib_symm_apply`, `denselyOrdered_of_noMaxOrder`, `Prod.Lex.sumLexProdLexDistrib_apply`, `denselyOrdered_of_noMinOrder`, `inl_lt_inl_iff`, `lt_def`, `toLexRelIsoLT_coe`, `inl_lt_inr`, `toLexRelIsoLT_symm_coe`, `noMinOrder`, `inr_lt_inr_iff`, `noMinOrder_of_nonempty`, `not_inr_lt_inl`
`boundedOrder` 📖	CompOp	—
`linearOrder` 📖	CompOp	1 math math: `OrderType.type_lex_sum`
`orderBot` 📖	CompOp	1 math math: `inl_bot`
`orderTop` 📖	CompOp	1 math math: `inr_top`
`partialOrder` 📖	CompOp	—
`preorder` 📖	CompOp	30 math math: `Icc_inr_inr`, `Ico_inl_inl`, `Ico_inr_inr`, `Ioo_inl_inr`, `Ioo_inr_inl`, `Iic_inr`, `inr_strictMono`, `Ioo_inr_inr`, `Icc_inl_inl`, `inl_mono`, `Ioi_inr`, `Ici_inl`, `Ioc_inl_inl`, `Icc_inr_inl`, `Ioc_inl_inr`, `Iio_inl`, `Ioc_inr_inl`, `Ioc_inr_inr`, `Ioi_inl`, `Ioo_inl_inl`, `Iic_inl`, `inl_strictMono`, `Ici_inr`, `Ico_inr_inl`, `Ico_inl_inr`, `Iio_inr`, `inr_mono`, `toLex_strictMono`, `Icc_inl_inr`, `toLex_mono`
`toLexRelIsoLE` 📖	CompOp	2 math math: `toLexRelIsoLE_coe`, `toLexRelIsoLE_symm_coe`
`toLexRelIsoLT` 📖	CompOp	2 math math: `toLexRelIsoLT_coe`, `toLexRelIsoLT_symm_coe`
`«term_⊕ₗ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`denselyOrdered_of_noMaxOrder` 📖	mathematical	—	`DenselyOrdered` `Lex` `LT`	—	`exists_between` `inl_lt_inl_iff` `NoMaxOrder.exists_gt` `inl_lt_inr` `inr_lt_inr_iff`
`denselyOrdered_of_noMinOrder` 📖	mathematical	—	`DenselyOrdered` `Lex` `LT`	—	`exists_between` `inl_lt_inl_iff` `NoMinOrder.exists_lt` `inl_lt_inr` `inr_lt_inr_iff`
`inl_bot` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Bot.bot` `OrderBot.toBot` `LE` `orderBot`	—	—
`inl_le_inl_iff` 📖	mathematical	—	`Lex` `LE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`inl_le_inr` 📖	mathematical	—	`Lex` `LE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`inl_lt_inl_iff` 📖	mathematical	—	`Lex` `LT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`inl_lt_inr` 📖	mathematical	—	`Lex` `LT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`inl_mono` 📖	mathematical	—	`Monotone` `Lex` `preorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`Monotone.comp` `toLex_mono` `Sum.inl_mono`
`inl_strictMono` 📖	mathematical	—	`StrictMono` `Lex` `preorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`StrictMono.comp` `toLex_strictMono` `Sum.inl_strictMono`
`inr_le_inr_iff` 📖	mathematical	—	`Lex` `LE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`inr_lt_inr_iff` 📖	mathematical	—	`Lex` `LT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`inr_mono` 📖	mathematical	—	`Monotone` `Lex` `preorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`Monotone.comp` `toLex_mono` `Sum.inr_mono`
`inr_strictMono` 📖	mathematical	—	`StrictMono` `Lex` `preorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`StrictMono.comp` `toLex_strictMono` `Sum.inr_strictMono`
`inr_top` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Top.top` `OrderTop.toTop` `LE` `orderTop`	—	—
`le_def` 📖	mathematical	—	`Lex` `LE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`lt_def` 📖	mathematical	—	`Lex` `LT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`noMaxOrder` 📖	mathematical	—	`NoMaxOrder` `Lex` `LT`	—	`NoMaxOrder.exists_gt` `inl_lt_inl_iff` `inr_lt_inr_iff`
`noMaxOrder_of_nonempty` 📖	mathematical	—	`NoMaxOrder` `Lex` `LT`	—	`inl_lt_inr` `NoMaxOrder.exists_gt` `inr_lt_inr_iff`
`noMinOrder` 📖	mathematical	—	`NoMinOrder` `Lex` `LT`	—	`NoMinOrder.exists_lt` `inl_lt_inl_iff` `inr_lt_inr_iff`
`noMinOrder_of_nonempty` 📖	mathematical	—	`NoMinOrder` `Lex` `LT`	—	`NoMinOrder.exists_lt` `inl_lt_inl_iff` `inl_lt_inr`
`not_inr_le_inl` 📖	mathematical	—	`Lex` `LE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`not_inr_lt_inl` 📖	mathematical	—	`Lex` `LT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`toLexRelIsoLE_coe` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Lex` `LE` `RelIso.instFunLike` `toLexRelIsoLE` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`toLexRelIsoLE_symm_coe` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Lex` `LE` `RelIso.instFunLike` `RelIso.symm` `toLexRelIsoLE` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`toLexRelIsoLT_coe` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Lex` `LT` `RelIso.instFunLike` `toLexRelIsoLT` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`toLexRelIsoLT_symm_coe` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Lex` `LT` `RelIso.instFunLike` `RelIso.symm` `toLexRelIsoLT` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex`	—	—
`toLex_le_toLex` 📖	mathematical	—	`Lex` `LE` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`toLex_lt_toLex` 📖	mathematical	—	`Lex` `LT` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`toLex_mono` 📖	mathematical	—	`Monotone` `Lex` `Sum.instPreorderSum` `preorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`toLex_strictMono` 📖	mathematical	—	`StrictMono` `Lex` `Sum.instPreorderSum` `preorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—

Sum.LiftRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`refl` 📖	—	—	—	—	`refl`
`trans` 📖	—	—	—	—	`trans`

WithBot

Definitions

Name	Category	Theorems
`orderIsoPUnitSumLex` 📖	CompOp	4 math math: `orderIsoPUnitSumLex_symm_inl`, `orderIsoPUnitSumLex_symm_inr`, `orderIsoPUnitSumLex_toLex`, `orderIsoPUnitSumLex_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderIsoPUnitSumLex_bot` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithBot` `Lex` `instLE` `Sum.Lex.LE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `PUnit.instBiheytingAlgebra` `instFunLikeOrderIso` `orderIsoPUnitSumLex` `Bot.bot` `bot` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`orderIsoPUnitSumLex_symm_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `WithBot` `Sum.Lex.LE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `PUnit.instBiheytingAlgebra` `instLE` `instFunLikeOrderIso` `OrderIso.symm` `orderIsoPUnitSumLex` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Bot.bot` `bot`	—	—
`orderIsoPUnitSumLex_symm_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `WithBot` `Sum.Lex.LE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `PUnit.instBiheytingAlgebra` `instLE` `instFunLikeOrderIso` `OrderIso.symm` `orderIsoPUnitSumLex` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `some`	—	—
`orderIsoPUnitSumLex_toLex` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithBot` `Lex` `instLE` `Sum.Lex.LE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `PUnit.instBiheytingAlgebra` `instFunLikeOrderIso` `orderIsoPUnitSumLex` `some` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—

WithTop

Definitions

Name	Category	Theorems
`orderIsoSumLexPUnit` 📖	CompOp	4 math math: `orderIsoSumLexPUnit_toLex`, `orderIsoSumLexPUnit_symm_inl`, `orderIsoSumLexPUnit_top`, `orderIsoSumLexPUnit_symm_inr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderIsoSumLexPUnit_symm_inl` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `WithTop` `Sum.Lex.LE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `PUnit.instBiheytingAlgebra` `instLE` `instFunLikeOrderIso` `OrderIso.symm` `orderIsoSumLexPUnit` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `some`	—	—
`orderIsoSumLexPUnit_symm_inr` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Lex` `WithTop` `Sum.Lex.LE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `PUnit.instBiheytingAlgebra` `instLE` `instFunLikeOrderIso` `OrderIso.symm` `orderIsoSumLexPUnit` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `Top.top` `top`	—	—
`orderIsoSumLexPUnit_toLex` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithTop` `Lex` `instLE` `Sum.Lex.LE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `PUnit.instBiheytingAlgebra` `instFunLikeOrderIso` `orderIsoSumLexPUnit` `some` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—
`orderIsoSumLexPUnit_top` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `WithTop` `Lex` `instLE` `Sum.Lex.LE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `PUnit.instBiheytingAlgebra` `instFunLikeOrderIso` `orderIsoSumLexPUnit` `Top.top` `top` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	—

---

← Back to Index