Documentation Verification Report

ScottContinuity

📁 Source: Mathlib/Order/ScottContinuity.lean

Statistics

Metric	Count
Definitions `ScottContinuous`, `ScottContinuousOn`	2
Theorems `comp`, `const`, `fst`, `fun_comp`, `fun_const`, `fun_id`, `id`, `monotone`, `prodMk`, `scottContinuousOn`, `snd`, `sup₂`, `comp`, `const`, `fst`, `fun_comp`, `fun_const`, `fun_id`, `fun_image_comp`, `id`, `image_comp`, `mono`, `monotone`, `prodMk`, `snd`, `sup₂`, `scottContinuousOn_univ`	27
Total	29

ScottContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`ScottContinuous`	—	—	`scottContinuousOn_univ` `ScottContinuousOn.comp`
`const` 📖	mathematical	—	`ScottContinuous`	—	—
`fst` 📖	mathematical	—	`ScottContinuous` `Prod.instPreorder`	—	—
`fun_comp` 📖	—	`ScottContinuous`	—	—	`comp`
`fun_const` 📖	mathematical	—	`ScottContinuous`	—	`const`
`fun_id` 📖	mathematical	—	`ScottContinuous`	—	`id`
`id` 📖	mathematical	—	`ScottContinuous`	—	`Set.image_congr` `Set.image_id'`
`monotone` 📖	mathematical	`ScottContinuous`	`Monotone`	—	`ScottContinuousOn.monotone` `Set.mem_univ` `scottContinuousOn`
`prodMk` 📖	mathematical	`ScottContinuous`	`Prod.instPreorder`	—	`scottContinuousOn_univ` `ScottContinuousOn.prodMk`
`scottContinuousOn` 📖	mathematical	`ScottContinuous`	`ScottContinuousOn`	—	—
`snd` 📖	mathematical	—	`ScottContinuous` `Prod.instPreorder`	—	—
`sup₂` 📖	mathematical	—	`ScottContinuous` `Prod.instPreorder` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`sup_le_sup` `sup_le_iff`

ScottContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`Set` `Set.instMembership` `Set.instInsert` `Set.instSingletonSet` `Set.MapsTo` `Set.image` `ScottContinuousOn`	—	—	`monotone` `Set.image_comp`
`const` 📖	mathematical	—	`ScottContinuousOn`	—	`Set.image_congr`
`fst` 📖	mathematical	—	`ScottContinuousOn` `Prod.instPreorder`	—	—
`fun_comp` 📖	—	`Set` `Set.instMembership` `Set.instInsert` `Set.instSingletonSet` `Set.MapsTo` `Set.image` `ScottContinuousOn`	—	—	`comp`
`fun_const` 📖	mathematical	—	`ScottContinuousOn`	—	`const`
`fun_id` 📖	mathematical	—	`ScottContinuousOn`	—	`id`
`fun_image_comp` 📖	—	`Set` `Set.instMembership` `Set.instInsert` `Set.instSingletonSet` `ScottContinuousOn` `Set.image`	—	—	`image_comp`
`id` 📖	mathematical	—	`ScottContinuousOn`	—	`Set.image_congr` `Set.image_id'`
`image_comp` 📖	—	`Set` `Set.instMembership` `Set.instInsert` `Set.instSingletonSet` `ScottContinuousOn` `Set.image`	—	—	`comp` `Set.mapsTo_image`
`mono` 📖	—	`Set` `Set.instHasSubset` `ScottContinuousOn`	—	—	—
`monotone` 📖	mathematical	`Set` `Set.instMembership` `Set.instInsert` `Set.instSingletonSet` `ScottContinuousOn`	`Monotone`	—	`Set.insert_nonempty` `directedOn_pair` `le_refl` `IsLUB.eq_1` `upperBounds_insert` `upperBounds_singleton` `Set.inter_eq_self_of_subset_right` `Set.Ici_subset_Ici` `isLeast_Ici` `Set.mem_image_of_mem` `Set.mem_insert`
`prodMk` 📖	mathematical	`Set` `Set.instMembership` `Set.instInsert` `Set.instSingletonSet` `ScottContinuousOn`	`Prod.instPreorder`	—	`IsLUB.eq_1` `IsLeast.eq_1` `upperBounds.eq_1` `monotone` `isLUB_le_iff`
`snd` 📖	mathematical	—	`ScottContinuousOn` `Prod.instPreorder`	—	—
`sup₂` 📖	mathematical	—	`ScottContinuousOn` `Prod.instPreorder` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`ScottContinuous.scottContinuousOn` `ScottContinuous.sup₂`

(root)

Definitions

Name	Category	Theorems
`ScottContinuous` 📖	MathDef	15 math math: `ScottContinuous.fun_id`, `scottContinuous_inf_right`, `Topology.IsScott.isOpen_iff_scottContinuous_mem`, `scottContinuousOn_univ`, `ScottContinuous.inf₂`, `ScottContinuous.fst`, `ScottContinuous.const`, `scottContinuous_inf_left`, `CompletePartialOrder.scottContinuous`, `ScottContinuous.sup₂`, `ScottContinuous.id`, `ScottContinuous.of_map_sSup`, `scottContinuous_iff_map_sSup`, `ScottContinuous.snd`, `ScottContinuous.fun_const`
`ScottContinuousOn` 📖	MathDef	10 math math: `ScottContinuousOn.const`, `ScottContinuousOn.snd`, `scottContinuousOn_univ`, `ScottContinuousOn.sup₂`, `ScottContinuousOn.fst`, `ScottContinuousOn.fun_const`, `ScottContinuousOn.id`, `ScottContinuousOn.fun_id`, `Topology.IsScott.scottContinuousOn_iff_continuous`, `ScottContinuous.scottContinuousOn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scottContinuousOn_univ` 📖	mathematical	—	`ScottContinuousOn` `Set.univ` `Set` `ScottContinuous`	—	—

---

← Back to Index