Defs

📁 Source: Mathlib/Order/Types/Defs.lean

Statistics

Metric	Count
Definitions `OrderType`, `ToType`, `instInhabited`, `instLinearOrderToType`, `instOne`, `instOrderBot`, `instPreorder`, `instSetoid`, `instZero`, `liftOn`, `liftOn₂`, `omega0`, `termω`, `type`	14
Theorems `type_le_type`, `type_congr`, `bot_eq_zero`, `inductionOn`, `inductionOn₂`, `inductionOn₃`, `instNeZeroOfNat`, `instNontrivial`, `liftOn_type`, `liftOn₂_type`, `not_lt_zero`, `pos_iff_ne_zero`, `type_congr`, `type_eq_one`, `type_eq_type`, `type_eq_zero`, `type_le_type`, `type_le_type_iff`, `type_lt_type`, `type_nat`, `type_ne_zero`, `type_ne_zero_iff`, `type_of_isEmpty`, `type_of_unique`, `type_toType`, `zero_le`	26
Total	40

OrderEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`type_le_type` 📖	mathematical	—	`OrderType` `Preorder.toLE` `OrderType.instPreorder` `OrderType.type`	—	`OrderType.type_le_type`

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`type_congr` 📖	mathematical	—	`OrderType.type`	—	`OrderType.type_congr`

OrderType

Definitions

Name	Category	Theorems
`ToType` 📖	CompOp	1 math math: `type_toType`
`instInhabited` 📖	CompOp	—
`instLinearOrderToType` 📖	CompOp	1 math math: `type_toType`
`instOne` 📖	CompOp	4 math math: `instZeroLEOneClass`, `type_of_unique`, `type_eq_one`, `instNeZeroOfNat`
`instOrderBot` 📖	CompOp	1 math math: `bot_eq_zero`
`instPreorder` 📖	CompOp	9 math math: `type_le_type`, `instZeroLEOneClass`, `type_lt_type`, `not_lt_zero`, `type_le_type_iff`, `zero_le`, `bot_eq_zero`, `pos_iff_ne_zero`, `OrderEmbedding.type_le_type`
`instSetoid` 📖	CompOp	—
`instZero` 📖	CompOp	8 math math: `instZeroLEOneClass`, `type_of_isEmpty`, `type_eq_zero`, `not_lt_zero`, `instNeZeroOfNat`, `zero_le`, `bot_eq_zero`, `pos_iff_ne_zero`
`liftOn` 📖	CompOp	1 math math: `liftOn_type`
`liftOn₂` 📖	CompOp	1 math math: `liftOn₂_type`
`omega0` 📖	CompOp	1 math math: `type_nat`
`termω` 📖	CompOp	—
`type` 📖	CompOp	17 math math: `type_le_type`, `type_of_unique`, `liftOn_type`, `type_lex_prod`, `type_of_isEmpty`, `OrderIso.type_congr`, `type_eq_one`, `type_eq_zero`, `type_eq_type`, `type_lt_type`, `type_le_type_iff`, `liftOn₂_type`, `type_lex_sum`, `type_congr`, `OrderEmbedding.type_le_type`, `type_toType`, `type_nat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_eq_zero` 📖	mathematical	—	`Bot.bot` `OrderType` `OrderBot.toBot` `Preorder.toLE` `instPreorder` `instOrderBot` `instZero`	—	—
`inductionOn` 📖	—	`type`	—	—	—
`inductionOn₂` 📖	—	`type`	—	—	—
`inductionOn₃` 📖	—	`type`	—	—	—
`instNeZeroOfNat` 📖	mathematical	—	`OrderType` `instZero` `instOne`	—	`type_ne_zero`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `OrderType`	—	`type_ne_zero`
`liftOn_type` 📖	mathematical	—	`liftOn` `type`	—	—
`liftOn₂_type` 📖	mathematical	—	`liftOn₂` `type`	—	—
`not_lt_zero` 📖	mathematical	—	`OrderType` `Preorder.toLT` `instPreorder` `instZero`	—	`not_lt_bot`
`pos_iff_ne_zero` 📖	mathematical	—	`OrderType` `Preorder.toLT` `instPreorder` `instZero`	—	`ne_bot_of_gt` `type_toType` `PEmpty.instIsEmpty` `instIsEmptyForallOfNonempty`
`type_congr` 📖	mathematical	—	`type`	—	`type_eq_type`
`type_eq_one` 📖	mathematical	—	`type` `OrderType` `instOne` `Unique`	—	`type_eq_type` `type_of_unique` `Unique.instSubsingleton`
`type_eq_type` 📖	mathematical	—	`type` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Quotient.eq'`
`type_eq_zero` 📖	mathematical	—	`type` `OrderType` `instZero` `IsEmpty`	—	`type_eq_type` `Equiv.isEmpty` `PEmpty.instIsEmpty` `type_of_isEmpty`
`type_le_type` 📖	mathematical	—	`OrderType` `Preorder.toLE` `instPreorder` `type`	—	—
`type_le_type_iff` 📖	mathematical	—	`OrderType` `Preorder.toLE` `instPreorder` `type` `OrderEmbedding` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—
`type_lt_type` 📖	mathematical	—	`OrderType` `Preorder.toLT` `instPreorder` `type`	—	`not_nonempty_iff`
`type_nat` 📖	mathematical	—	`type` `Nat.instLinearOrder` `omega0`	—	`type_congr`
`type_ne_zero` 📖	—	—	—	—	`type_ne_zero_iff`
`type_ne_zero_iff` 📖	—	—	—	—	—
`type_of_isEmpty` 📖	mathematical	—	`type` `OrderType` `instZero`	—	`type_congr` `PEmpty.instIsEmpty`
`type_of_unique` 📖	mathematical	—	`type` `OrderType` `instOne`	—	`nonempty_unique` `OrderIso.type_congr`
`type_toType` 📖	mathematical	—	`type` `ToType` `instLinearOrderToType`	—	`Function.surjInv_eq`
`zero_le` 📖	mathematical	—	`OrderType` `Preorder.toLE` `instPreorder` `instZero`	—	`inductionOn` `OrderEmbedding.type_le_type` `PEmpty.instIsEmpty`

(root)

Definitions

Name	Category	Theorems
`OrderType` 📖	CompOp	18 math math: `OrderType.type_le_type`, `OrderType.instZeroLEOneClass`, `OrderType.type_of_unique`, `OrderType.type_lex_prod`, `OrderType.type_of_isEmpty`, `OrderType.type_eq_one`, `OrderType.type_eq_zero`, `OrderType.instLeftDistribClass`, `OrderType.type_lt_type`, `OrderType.not_lt_zero`, `OrderType.instNeZeroOfNat`, `OrderType.type_le_type_iff`, `OrderType.zero_le`, `OrderType.bot_eq_zero`, `OrderType.instNontrivial`, `OrderType.type_lex_sum`, `OrderType.pos_iff_ne_zero`, `OrderEmbedding.type_le_type`

---

← Back to Index