Documentation Verification Report

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`, `exists_ge`, `exists_le`, `exists_ge`, `exists_le`	8
Total	23

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`
`exists_ge` 📖	mathematical	—	`Preorder.toLE`	—	`Directed.finite_le` `instIsTransGe` `directed_id`
`exists_le` 📖	mathematical	—	`Preorder.toLE`	—	`Directed.finite_le` `instIsTransLe` `directed_id`

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