Documentation Verification Report

Lattice

📁 Source: Mathlib/Algebra/Order/Nonneg/Lattice.lean

Statistics

Metric	Count
Definitions `conditionallyCompleteLinearOrder`, `conditionallyCompleteLinearOrderBot`, `distribLattice`, `orderBot`, `semilatticeInf`, `semilatticeSup`	6
Theorems `bot_eq`, `instDenselyOrdered`, `noMaxOrder`	3
Total	9

Nonneg

Definitions

Name	Category	Theorems
`conditionallyCompleteLinearOrder` 📖	CompOp	—
`conditionallyCompleteLinearOrderBot` 📖	CompOp	—
`distribLattice` 📖	CompOp	1 math math: `segment_eq_uIcc`
`orderBot` 📖	CompOp	1 math math: `bot_eq`
`semilatticeInf` 📖	CompOp	—
`semilatticeSup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_eq` 📖	mathematical	—	`Bot.bot` `Preorder.toLE` `OrderBot.toBot` `orderBot` `le_rfl`	—	—
`instDenselyOrdered` 📖	mathematical	—	`DenselyOrdered` `Preorder.toLE` `Preorder.toLT`	—	`Set.instDenselyOrdered` `Set.ordConnected_Ici`
`noMaxOrder` 📖	mathematical	—	`NoMaxOrder` `Preorder.toLE` `PartialOrder.toPreorder` `Preorder.toLT`	—	`Set.instNoMaxOrderElemIci`

---

← Back to Index