Documentation Verification Report

Complete

📁 Source: Mathlib/Order/ScottContinuity/Complete.lean

Statistics

Metric	Count
Definitions	0
Theorems `inf₂`, `map_sSup`, `of_map_sSup`, `scottContinuous_iff_map_sSup`, `scottContinuous_inf_left`, `scottContinuous_inf_right`	6
Total	6

ScottContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inf₂` 📖	mathematical	—	`ScottContinuous` `Prod.instPreorder` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice`	—	`fromProd` `scottContinuous_inf_right` `scottContinuous_inf_left`
`map_sSup` 📖	mathematical	`ScottContinuous` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `Set.Nonempty` `DirectedOn` `Preorder.toLE`	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set.image`	—	`scottContinuous_iff_map_sSup`
`of_map_sSup` 📖	mathematical	`SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set.image`	`ScottContinuous` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf`	—	`scottContinuous_iff_map_sSup`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scottContinuous_iff_map_sSup` 📖	mathematical	—	`ScottContinuous` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `Set.image`	—	`IsLUB.sSup_eq` `isLUB_iff_sSup_eq`
`scottContinuous_inf_left` 📖	mathematical	—	`ScottContinuous` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice`	—	`ScottContinuous.of_map_sSup` `sSup_inf_eq` `sSup_image`
`scottContinuous_inf_right` 📖	mathematical	—	`ScottContinuous` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice`	—	`ScottContinuous.of_map_sSup` `inf_sSup_eq` `sSup_image`

---

← Back to Index