Order

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

Statistics

Metric	Count
Definitions `completeAtomicBooleanAlgebra`, `completeBooleanAlgebra`, `completeLinearOrder`, `completeLinearOrder`, `toBoundedOrder`, `toCompleteAtomicBooleanAlgebra`, `toCompleteBooleanAlgebra`, `toCompleteDistribLattice`, `toCompleteDistribLatticeMinimalAxioms`, `toCompleteLattice`, `toCompleteLatticeOfNonempty`, `toCompleteLinearOrder`, `toCompleteLinearOrderOfNonempty`, `toOrderBot`, `toOrderTop`	15
Theorems `finite_le`, `finite_set_le`, `bddAbove_range`, `bddBelow_range`, `ciInf_inf`, `ciInf_le`, `ciInf_le_of_le`, `ciInf_mono`, `ciInf_prod`, `ciSup_mono`, `ciSup_prod`, `ciSup_sup`, `exists_ge`, `exists_le`, `le_ciSup`, `le_ciSup_of_le`, `map_iInf_of_antitone`, `map_iInf_of_antitoneOn`, `map_iInf_of_monotone`, `map_iInf_of_monotoneOn`, `map_iSup_of_antitone`, `map_iSup_of_antitoneOn`, `map_iSup_of_monotone`, `map_iSup_of_monotoneOn`, `exists_ge`, `exists_le`	26
Total	41

Bool

Definitions

Name	Category	Theorems
`completeAtomicBooleanAlgebra` 📖	CompOp	—
`completeBooleanAlgebra` 📖	CompOp	—
`completeLinearOrder` 📖	CompOp	—

Directed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_le` 📖	—	`Directed`	—	—	`finite_set_le` `Set.finite_range`
`finite_set_le` 📖	—	`Directed`	—	—	`Set.Finite.mem_toFinset` `finset_le`

Fin

Definitions

Name	Category	Theorems
`completeLinearOrder` 📖	CompOp	—

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove_range` 📖	mathematical	—	`BddAbove` `Preorder.toLE` `Set.range`	—	`exists_le`
`bddBelow_range` 📖	mathematical	—	`BddBelow` `Preorder.toLE` `Set.range`	—	`exists_ge`
`ciInf_inf` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`ciSup_sup`
`ciInf_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`le_ciSup`
`ciInf_le_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`ciInf_le_of_le` `bddBelow_range` `supSet_to_nonempty` `SemilatticeInf.instIsCodirectedOrder`
`ciInf_mono` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`ciInf_mono` `bddBelow_range` `supSet_to_nonempty` `SemilatticeInf.instIsCodirectedOrder`
`ciInf_prod` 📖	mathematical	—	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`ciSup_prod`
`ciSup_mono` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`ciSup_mono` `bddAbove_range` `supSet_to_nonempty` `SemilatticeSup.instIsDirectedOrder`
`ciSup_prod` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`ciSup_prod` `bddAbove_range` `instProd` `supSet_to_nonempty` `SemilatticeSup.instIsDirectedOrder`
`ciSup_sup` 📖	mathematical	—	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`le_antisymm` `sup_le` `ciSup_le` `le_ciSup_of_le` `le_sup_left` `le_sup_right` `sup_le_sup_right` `le_ciSup`
`exists_ge` 📖	mathematical	—	`Preorder.toLE`	—	`Directed.finite_le` `instIsTransGe` `directed_id`
`exists_le` 📖	mathematical	—	`Preorder.toLE`	—	`Directed.finite_le` `instIsTransLe` `directed_id`
`le_ciSup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`le_ciSup_of_le` `le_rfl`
`le_ciSup_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`le_ciSup_of_le` `bddAbove_range` `supSet_to_nonempty` `SemilatticeSup.instIsDirectedOrder`
`map_iInf_of_antitone` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup`	—	`map_iInf_of_monotone`
`map_iInf_of_antitoneOn` 📖	mathematical	`AntitoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup`	—	`map_iInf_of_monotoneOn`
`map_iInf_of_monotone` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`map_iSup_of_monotone`
`map_iInf_of_monotoneOn` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`map_iSup_of_monotoneOn`
`map_iSup_of_antitone` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`map_iSup_of_monotone`
`map_iSup_of_antitoneOn` 📖	mathematical	`AntitoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`map_iSup_of_monotoneOn`
`map_iSup_of_monotone` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`map_iSup_of_monotoneOn` `monotoneOn_univ` `Set.mem_univ`
`map_iSup_of_monotoneOn` 📖	mathematical	`MonotoneOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`exists_eq_ciSup_of_finite` `le_antisymm` `le_ciSup_of_le` `le_rfl` `ciSup_le` `le_ciSup`

Fintype

Definitions

Name	Category	Theorems
`toBoundedOrder` 📖	CompOp	—
`toCompleteAtomicBooleanAlgebra` 📖	CompOp	—
`toCompleteBooleanAlgebra` 📖	CompOp	—
`toCompleteDistribLattice` 📖	CompOp	—
`toCompleteDistribLatticeMinimalAxioms` 📖	CompOp	—
`toCompleteLattice` 📖	CompOp	—
`toCompleteLatticeOfNonempty` 📖	CompOp	—
`toCompleteLinearOrder` 📖	CompOp	—
`toCompleteLinearOrderOfNonempty` 📖	CompOp	—
`toOrderBot` 📖	CompOp	—
`toOrderTop` 📖	CompOp	—

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_ge` 📖	mathematical	—	`Preorder.toLE`	—	`Directed.finite_set_le` `instIsTransGe` `directed_id`
`exists_le` 📖	mathematical	—	`Preorder.toLE`	—	`Directed.finite_set_le` `instIsTransLe` `directed_id`

---

← Back to Index