Documentation Verification Report

CompletePartialOrder

📁 Source: Mathlib/Order/CompletePartialOrder.lean

Statistics

Metric	Count
Definitions `toCompletePartialOrder`, `CompletePartialOrder`, `toOmegaCompletePartialOrder`, `toPartialOrder`, `toSupSet`, `instConditionallyCompletePartialOrderSupOfCompletePartialOrder`	6
Theorems `lubOfDirected`, `scottContinuous`, `iSup_le`, `le_iSup`, `isLUB_sSup`, `le_sSup`, `sSup_le`	7
Total	13

CompleteLattice

Definitions

Name	Category	Theorems
`toCompletePartialOrder` 📖	CompOp	7 math math: `MeasureTheory.isTightMeasureSet_iff_inner_tendsto`, `MeasureTheory.tendsto_measure_norm_gt_of_isTightMeasureSet`, `EMetric.pair_reduction`, `MeasureTheory.tendsto_measure_compl_closedBall_of_isTightMeasureSet`, `MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt`, `PairReduction.iSup_edist_pairSet`, `MeasureTheory.isTightMeasureSet_iff_tendsto_measure_compl_closedBall`

CompletePartialOrder

Definitions

Name	Category	Theorems
`toOmegaCompletePartialOrder` 📖	CompOp	—
`toPartialOrder` 📖	CompOp	1 math math: `scottContinuous`
`toSupSet` 📖	CompOp	14 math math: `MeasureTheory.isTightMeasureSet_iff_inner_tendsto`, `DirectedOn.isLUB_sSup`, `MeasureTheory.tendsto_measure_norm_gt_of_isTightMeasureSet`, `DirectedOn.sSup_le`, `Directed.iSup_le`, `EMetric.pair_reduction`, `scottContinuous`, `Directed.le_iSup`, `MeasureTheory.tendsto_measure_compl_closedBall_of_isTightMeasureSet`, `MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt`, `lubOfDirected`, `PairReduction.iSup_edist_pairSet`, `MeasureTheory.isTightMeasureSet_iff_tendsto_measure_compl_closedBall`, `DirectedOn.le_sSup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lubOfDirected` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `toPartialOrder`	`IsLUB` `SupSet.sSup` `toSupSet`	—	—
`scottContinuous` 📖	mathematical	—	`ScottContinuous` `PartialOrder.toPreorder` `toPartialOrder` `IsLUB` `Preorder.toLE` `Set.image` `SupSet.sSup` `toSupSet`	—	`DirectedOn.isLUB_sSup` `IsLUB.unique`

Directed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup_le` 📖	mathematical	`Directed` `Preorder.toLE` `PartialOrder.toPreorder` `CompletePartialOrder.toPartialOrder`	`iSup` `CompletePartialOrder.toSupSet`	—	`DirectedOn.sSup_le` `directedOn_range` `Set.forall_mem_range`
`le_iSup` 📖	mathematical	`Directed` `Preorder.toLE` `PartialOrder.toPreorder` `CompletePartialOrder.toPartialOrder`	`iSup` `CompletePartialOrder.toSupSet`	—	`DirectedOn.le_sSup` `directedOn_range` `Set.mem_range_self`

DirectedOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLUB_sSup` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `CompletePartialOrder.toPartialOrder`	`IsLUB` `SupSet.sSup` `CompletePartialOrder.toSupSet`	—	`CompletePartialOrder.lubOfDirected`
`le_sSup` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `CompletePartialOrder.toPartialOrder` `Set` `Set.instMembership`	`SupSet.sSup` `CompletePartialOrder.toSupSet`	—	`isLUB_sSup`
`sSup_le` 📖	mathematical	`DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `CompletePartialOrder.toPartialOrder`	`SupSet.sSup` `CompletePartialOrder.toSupSet`	—	`isLUB_sSup`

(root)

Definitions

Name	Category	Theorems
`CompletePartialOrder` 📖	CompData	—
`instConditionallyCompletePartialOrderSupOfCompletePartialOrder` 📖	CompOp	—

---

← Back to Index