Documentation Verification Report

Basic

📁 Source: Mathlib/Order/ConditionallyCompletePartialOrder/Basic.lean

Statistics

Metric	Count
Definitions `instConditionallyCompletePartialOrder`, `instConditionallyCompletePartialOrderInfOfConditionallyCompletePartialOrderSup`, `instConditionallyCompletePartialOrderSupOfConditionallyCompletePartialOrderInf`	3
Theorems `csInf_eq_of_forall_ge_of_forall_gt_exists_lt`, `csInf_le_csInf`, `csInf_le_csSup`, `csInf_le_iff`, `csInf_le_of_le`, `csInf_lt_of_lt`, `csSup_eq_of_forall_le_of_forall_lt_exists_gt`, `csSup_le_csSup`, `csSup_le_iff`, `le_csInf_iff`, `le_csSup_iff`, `le_csSup_of_le`, `lt_csSup_of_lt`, `notMem_of_csSup_lt`, `notMem_of_lt_csInf`, `subset_Icc_csInf_csSup`, `csSup_eq`, `csSup_mem`, `directedOn`, `csInf_eq`, `csInf_mem`, `directedOn`, `csInf_Icc`, `csInf_Ici`, `csInf_Ico`, `csInf_singleton`, `csSup_Icc`, `csSup_Iic`, `csSup_Ioc`, `csSup_singleton`, `inf_eq_bot_of_bot_mem`, `sup_eq_top_of_top_mem`	32
Total	35

DirectedOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`csInf_eq_of_forall_ge_of_forall_gt_exists_lt` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder` `Set.Nonempty` `Set` `Set.instMembership` `Preorder.toLT`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet`	—	`eq_of_le_of_not_lt'` `le_csInf` `lt_irrefl` `LT.lt.trans_le'` `csInf_le`
`csInf_le_csInf` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder` `BddBelow` `Set.Nonempty` `Set` `Set.instHasSubset`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet`	—	`le_csInf` `csInf_le`
`csInf_le_csSup` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `BddBelow` `BddAbove` `Set.Nonempty`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`isGLB_le_isLUB` `isGLB_csInf` `isLUB_csSup`
`csInf_le_iff` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder` `BddBelow` `Set.Nonempty`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet`	—	`ge_trans` `le_csInf` `csInf_le`
`csInf_le_of_le` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder` `BddBelow` `Set` `Set.instMembership`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet`	—	`ge_trans` `csInf_le`
`csInf_lt_of_lt` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder` `BddBelow` `Set` `Set.instMembership` `Preorder.toLT`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet`	—	`lt_of_lt_of_le'` `csInf_le`
`csSup_eq_of_forall_le_of_forall_lt_exists_gt` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `Set.Nonempty` `Set` `Set.instMembership` `Preorder.toLT`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`eq_of_le_of_not_lt` `csSup_le` `lt_irrefl` `LT.lt.trans_le` `le_csSup`
`csSup_le_csSup` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `BddAbove` `Set.Nonempty` `Set` `Set.instHasSubset`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`csSup_le` `le_csSup`
`csSup_le_iff` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `BddAbove` `Set.Nonempty`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`isLUB_le_iff` `isLUB_csSup`
`le_csInf_iff` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder` `BddBelow` `Set.Nonempty`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet`	—	`le_isGLB_iff` `isGLB_csInf`
`le_csSup_iff` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `BddAbove` `Set.Nonempty`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`le_trans` `csSup_le` `le_csSup`
`le_csSup_of_le` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `BddAbove` `Set` `Set.instMembership`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`le_trans` `le_csSup`
`lt_csSup_of_lt` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `BddAbove` `Set` `Set.instMembership` `Preorder.toLT`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`lt_of_lt_of_le` `le_csSup`
`notMem_of_csSup_lt` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `Preorder.toLT` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `BddAbove`	`Set` `Set.instMembership`	—	`lt_irrefl` `LE.le.trans_lt` `le_csSup`
`notMem_of_lt_csInf` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder` `Preorder.toLT` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `BddBelow`	`Set` `Set.instMembership`	—	`lt_irrefl` `LE.le.trans_lt'` `csInf_le`
`subset_Icc_csInf_csSup` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `BddBelow` `BddAbove`	`Set` `Set.instHasSubset` `Set.Icc` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`csInf_le` `le_csSup`

IsGreatest

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`csSup_eq` 📖	mathematical	`IsGreatest` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`IsLUB.unique` `DirectedOn.isLUB_csSup` `directedOn` `nonempty` `isLUB`
`csSup_mem` 📖	mathematical	`IsGreatest` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder`	`Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`csSup_eq`
`directedOn` 📖	mathematical	`IsGreatest` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder`	`DirectedOn`	—	—

IsLeast

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`csInf_eq` 📖	mathematical	`IsLeast` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet`	—	`IsGLB.unique` `DirectedOn.isGLB_csInf` `directedOn` `nonempty` `isGLB`
`csInf_mem` 📖	mathematical	`IsLeast` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder`	`Set` `Set.instMembership` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet`	—	`csInf_eq`
`directedOn` 📖	mathematical	`IsLeast` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder`	`DirectedOn`	—	—

OrderDual

Definitions

Name	Category	Theorems
`instConditionallyCompletePartialOrder` 📖	CompOp	—
`instConditionallyCompletePartialOrderInfOfConditionallyCompletePartialOrderSup` 📖	CompOp	—
`instConditionallyCompletePartialOrderSupOfConditionallyCompletePartialOrderInf` 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`csInf_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `Set.Icc`	—	`IsLeast.csInf_eq` `isLeast_Icc`
`csInf_Ici` 📖	mathematical	—	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `Set.Ici` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder`	—	`IsLeast.csInf_eq` `isLeast_Ici`
`csInf_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `Set.Ico`	—	`IsLeast.csInf_eq` `isLeast_Ico`
`csInf_singleton` 📖	mathematical	—	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `Set` `Set.instSingletonSet`	—	`IsLeast.csInf_eq` `isLeast_singleton`
`csSup_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.Icc`	—	`IsGreatest.csSup_eq` `isGreatest_Icc`
`csSup_Iic` 📖	mathematical	—	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.Iic` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder`	—	`IsGreatest.csSup_eq` `isGreatest_Iic`
`csSup_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.Ioc`	—	`IsGreatest.csSup_eq` `isGreatest_Ioc`
`csSup_singleton` 📖	mathematical	—	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instSingletonSet`	—	`IsGreatest.csSup_eq` `isGreatest_singleton`
`inf_eq_bot_of_bot_mem` 📖	mathematical	`Set` `Set.instMembership` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderInf.toPartialOrder`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet`	—	`IsLeast.csInf_eq` `bot_le`
`sup_eq_top_of_top_mem` 📖	mathematical	`Set` `Set.instMembership` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`IsGreatest.csSup_eq` `le_top`

---

← Back to Index