Documentation Verification Report

ScottTopology

📁 Source: Mathlib/Topology/Order/ScottTopology.lean

Statistics

Metric	Count
Definitions `IsScott`, `withScottHomeomorph`, `IsScottHausdorff`, `WithScott`, `instInhabited`, `instPreorder`, `instTopologicalSpace`, `ofScott`, `rec`, `toScott`, `scott`, `scottHausdorff`	12
Theorems `scottHausdorff_le`, `closure_singleton`, `dirSupClosed_of_isClosed`, `instClosedIicTopologyOfUnivSet`, `instT0Space`, `instUnivSetOfIsUpper`, `isClosed_iff_isLowerSet_and_dirSupClosed`, `isLowerSet_of_isClosed`, `isOpen_iff_Iic_compl_or_univ`, `isOpen_iff_isUpperSet_and_dirSupInaccOn`, `isOpen_iff_isUpperSet_and_scottHausdorff_open`, `isOpen_iff_scottContinuous_mem`, `isUpperSet_of_isOpen`, `lowerClosure_subset_closure`, `monotone_of_continuous`, `scottContinuousOn_iff_continuous`, `scottHausdorff_le`, `scott_eq_upper_of_completeLinearOrder`, `topology_eq`, `topology_eq_scott`, `dirSupClosed_of_isClosed`, `dirSupInaccOn_of_isOpen`, `isClosed_iff_dirSupClosed`, `isClosed_of_isUpperSet`, `isOpen_iff`, `isOpen_iff_dirSupInacc`, `isOpen_of_isLowerSet`, `topology_eq`, `topology_eq_scottHausdorff`, `instIsScottUnivSet`, `instNonempty`, `isOpen_iff_isUpperSet_and_scottHausdorff_open'`, `ofScott_inj`, `ofScott_symm_eq`, `ofScott_toScott`, `toScott_inj`, `toScott_ofScott`, `toScott_symm_eq`, `instIsScottHausdorff`, `scottHausdorff_le_lower`, `scottHausdorff_le_scott`, `upperSet_le_scott`	42
Total	54

Topology

Definitions

Name	Category	Theorems
`IsScott` 📖	CompData	2 math math: `IsScott.instUnivSetOfIsUpper`, `WithScott.instIsScottUnivSet`
`IsScottHausdorff` 📖	CompData	1 math math: `instIsScottHausdorff`
`WithScott` 📖	CompOp	10 math math: `WithScott.instNonempty`, `WithScott.toScott_ofScott`, `WithScott.ofScott_inj`, `WithScott.toScott_symm_eq`, `WithScott.isOpen_iff_isUpperSet_and_scottHausdorff_open'`, `WithScott.toScott_inj`, `WithScott.ofScott_symm_eq`, `WithScott.ofScott_toScott`, `WithScott.instIsScottUnivSet`, `lawsonOpen_iff_scottOpen_of_isUpperSet`
`scott` 📖	CompOp	6 math math: `lawson_le_scott`, `IsScott.topology_eq`, `upperSet_le_scott`, `scottHausdorff_le_scott`, `IsScott.topology_eq_scott`, `IsScott.scott_eq_upper_of_completeLinearOrder`
`scottHausdorff` 📖	CompOp	11 math math: `scottHausdorff_le_isLawson`, `WithScott.isOpen_iff_isUpperSet_and_scottHausdorff_open'`, `scottHausdorff_le_lawson`, `IsScottHausdorff.topology_eq_scottHausdorff`, `IsScott.scottHausdorff_le`, `scottHausdorff_le_scott`, `scottHausdorff_le_lower`, `instIsScottHausdorff`, `IsScottHausdorff.topology_eq`, `IsLower.scottHausdorff_le`, `IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScottHausdorff` 📖	mathematical	—	`IsScottHausdorff` `scottHausdorff`	—	—
`scottHausdorff_le_lower` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `scottHausdorff` `Set.univ` `Set` `lower`	—	`IsScottHausdorff.isOpen_of_isLowerSet` `instIsScottHausdorff` `IsLower.isLowerSet_of_isOpen` `instIsLowerWithLower`
`scottHausdorff_le_scott` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `scottHausdorff` `Set.univ` `Set` `scott`	—	`le_sup_right`
`upperSet_le_scott` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `upperSet` `scott` `Set.univ` `Set`	—	`le_sup_left`

Topology.IsLower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scottHausdorff_le` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `Topology.scottHausdorff` `Set.univ` `Set`	—	`Topology.IsScottHausdorff.isOpen_of_isLowerSet` `Topology.instIsScottHausdorff` `isLowerSet_of_isOpen`

Topology.IsScott

Definitions

Name	Category	Theorems
`withScottHomeomorph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_singleton` 📖	mathematical	—	`closure` `Set` `Set.instSingletonSet` `Set.Iic`	—	`le_antisymm` `closure_minimal` `Set.singleton_subset_iff` `Set.mem_Iic` `le_refl` `isClosed_Iic` `instClosedIicTopologyOfUnivSet` `LowerSet.coe_Iic` `lowerClosure_singleton` `lowerClosure_subset_closure`
`dirSupClosed_of_isClosed` 📖	mathematical	—	`DirSupClosed`	—	`isClosed_iff_isLowerSet_and_dirSupClosed`
`instClosedIicTopologyOfUnivSet` 📖	mathematical	—	`ClosedIicTopology`	—	`isClosed_iff_isLowerSet_and_dirSupClosed` `isLowerSet_Iic` `dirSupClosed_Iic`
`instT0Space` 📖	mathematical	—	`T0Space`	—	`t0Space_iff_inseparable` `Set.Iic_injective` `closure_singleton`
`instUnivSetOfIsUpper` 📖	mathematical	—	`Topology.IsScott` `Set.univ` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot`	—	`scott_eq_upper_of_completeLinearOrder` `Topology.IsUpper.topology_eq`
`isClosed_iff_isLowerSet_and_dirSupClosed` 📖	mathematical	—	`IsClosed` `IsLowerSet` `Preorder.toLE` `DirSupClosed`	—	`isOpen_compl_iff` `isOpen_iff_isUpperSet_and_dirSupInaccOn` `isUpperSet_compl` `dirSupInaccOn_univ` `dirSupInacc_compl`
`isLowerSet_of_isClosed` 📖	mathematical	—	`IsLowerSet` `Preorder.toLE`	—	`isClosed_iff_isLowerSet_and_dirSupClosed`
`isOpen_iff_Iic_compl_or_univ` 📖	mathematical	—	`IsOpen` `Set.univ` `Compl.compl` `Set` `Set.instCompl` `Set.Iic` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot`	—	`Set.eq_empty_or_nonempty` `Set.compl_empty_iff` `compl_eq_comm` `le_antisymm_iff` `le_sSup` `IsLowerSet.Iic_subset` `isLowerSet_of_isClosed` `IsOpen.isClosed_compl` `dirSupClosed_iff_forall_sSup` `dirSupClosed_of_isClosed` `IsChain.directedOn` `instReflLe` `isChain_of_trichotomous` `instTrichotomousLe` `le_rfl` `isOpen_univ` `IsClosed.isOpen_compl` `isClosed_Iic` `instClosedIicTopologyOfUnivSet`
`isOpen_iff_isUpperSet_and_dirSupInaccOn` 📖	mathematical	—	`IsOpen` `IsUpperSet` `Preorder.toLE` `DirSupInaccOn`	—	`isOpen_iff_isUpperSet_and_scottHausdorff_open` `Topology.IsScottHausdorff.dirSupInaccOn_of_isOpen` `Topology.instIsScottHausdorff` `Set.Subset.trans` `Set.inter_subset_left` `IsUpperSet.Ici_subset`
`isOpen_iff_isUpperSet_and_scottHausdorff_open` 📖	mathematical	—	`IsOpen` `IsUpperSet` `Preorder.toLE` `Topology.scottHausdorff`	—	`topology_eq`
`isOpen_iff_scottContinuous_mem` 📖	mathematical	—	`IsOpen` `ScottContinuous` `PartialOrder.toPreorder` `Prop.partialOrder` `Set` `Set.instMembership`	—	`scottContinuousOn_univ` `scottContinuousOn_iff_continuous` `instUnivSetOfIsUpper` `instIsUpperProp` `isOpen_iff_continuous_mem`
`isUpperSet_of_isOpen` 📖	mathematical	`IsOpen`	`IsUpperSet` `Preorder.toLE`	—	`isOpen_iff_isUpperSet_and_scottHausdorff_open`
`lowerClosure_subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `LowerSet` `Preorder.toLE` `LowerSet.instSetLike` `lowerClosure` `closure`	—	`Topology.IsUpperSet.closure_eq_lowerClosure` `Topology.instIsUpperSet` `topology_eq` `closure.mono` `Topology.upperSet_le_scott`
`monotone_of_continuous` 📖	mathematical	`Continuous`	`Monotone`	—	`isUpperSet_of_isOpen` `IsOpen.preimage` `isOpen_compl_iff` `isClosed_Iic` `instClosedIicTopologyOfUnivSet`
`scottContinuousOn_iff_continuous` 📖	mathematical	`Set` `Set.instMembership` `Set.instInsert` `Set.instSingletonSet`	`ScottContinuousOn` `Continuous`	—	`continuous_def` `isOpen_iff_isUpperSet_and_dirSupInaccOn` `IsUpperSet.preimage` `isUpperSet_of_isOpen` `ScottContinuousOn.monotone` `Set.image_inter_nonempty_iff` `Set.Nonempty.image` `directedOn_image` `DirectedOn.mono` `Monotone.mem_upperBounds_image` `monotone_of_continuous` `IsOpen.preimage` `IsClosed.isOpen_compl` `isClosed_Iic` `instClosedIicTopologyOfUnivSet`
`scottHausdorff_le` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `Topology.scottHausdorff` `Set.univ` `Set`	—	`topology_eq` `Topology.scott.eq_1` `le_sup_right`
`scott_eq_upper_of_completeLinearOrder` 📖	mathematical	—	`Topology.scott` `Set.univ` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Topology.upper`	—	`TopologicalSpace.ext` `Topology.IsUpper.isTopologicalSpace_basis` `isOpen_iff_Iic_compl_or_univ`
`topology_eq` 📖	mathematical	—	`Topology.scott`	—	`topology_eq_scott`
`topology_eq_scott` 📖	mathematical	—	`Topology.scott`	—	—

Topology.IsScottHausdorff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dirSupClosed_of_isClosed` 📖	mathematical	—	`DirSupClosed`	—	`DirSupInacc.of_compl` `dirSupInaccOn_univ` `dirSupInaccOn_of_isOpen` `IsClosed.isOpen_compl`
`dirSupInaccOn_of_isOpen` 📖	mathematical	`IsOpen`	`DirSupInaccOn`	—	`isOpen_iff` `le_rfl`
`isClosed_iff_dirSupClosed` 📖	mathematical	—	`IsClosed` `DirSupClosed`	—	`isOpen_compl_iff` `isOpen_iff_dirSupInacc` `dirSupInacc_compl`
`isClosed_of_isUpperSet` 📖	mathematical	`IsUpperSet` `Preorder.toLE`	`IsClosed`	—	`isOpen_compl_iff` `isOpen_of_isLowerSet` `IsUpperSet.compl`
`isOpen_iff` 📖	mathematical	—	`IsOpen` `Set` `Set.instMembership` `Set.instHasSubset` `Set.instInter` `Set.Ici`	—	`topology_eq_scottHausdorff`
`isOpen_iff_dirSupInacc` 📖	mathematical	—	`IsOpen` `DirSupInacc`	—	`dirSupInaccOn_univ` `dirSupInaccOn_of_isOpen` `isOpen_iff` `Mathlib.Tactic.Push.not_and_eq` `Set.Nonempty.to_subtype` `Set.Nonempty.ne_empty` `Set.range_nonempty` `upperBounds_mono_set` `LE.le.trans` `Set.ext`
`isOpen_of_isLowerSet` 📖	mathematical	`IsLowerSet` `Preorder.toLE`	`IsOpen`	—	`isOpen_iff` `mem_upperBounds`
`topology_eq` 📖	mathematical	—	`Topology.scottHausdorff`	—	`topology_eq_scottHausdorff`
`topology_eq_scottHausdorff` 📖	mathematical	—	`Topology.scottHausdorff`	—	—

Topology.WithScott

Definitions

Name	Category	Theorems
`instInhabited` 📖	CompOp	—
`instPreorder` 📖	CompOp	1 math math: `instIsScottUnivSet`
`instTopologicalSpace` 📖	CompOp	3 math math: `isOpen_iff_isUpperSet_and_scottHausdorff_open'`, `instIsScottUnivSet`, `Topology.lawsonOpen_iff_scottOpen_of_isUpperSet`
`ofScott` 📖	CompOp	7 math math: `toScott_ofScott`, `ofScott_inj`, `toScott_symm_eq`, `isOpen_iff_isUpperSet_and_scottHausdorff_open'`, `ofScott_symm_eq`, `ofScott_toScott`, `Topology.lawsonOpen_iff_scottOpen_of_isUpperSet`
`rec` 📖	CompOp	—
`toScott` 📖	CompOp	5 math math: `toScott_ofScott`, `toScott_symm_eq`, `toScott_inj`, `ofScott_symm_eq`, `ofScott_toScott`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScottUnivSet` 📖	mathematical	—	`Topology.IsScott` `Topology.WithScott` `Set.univ` `Set` `instPreorder` `instTopologicalSpace`	—	—
`instNonempty` 📖	mathematical	—	`Topology.WithScott`	—	—
`isOpen_iff_isUpperSet_and_scottHausdorff_open'` 📖	mathematical	—	`IsOpen` `Topology.WithScott` `instTopologicalSpace` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofScott` `IsUpperSet` `Preorder.toLE` `TopologicalSpace.IsOpen` `Topology.scottHausdorff` `Set.univ` `Set`	—	—
`ofScott_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithScott` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofScott`	—	—
`ofScott_symm_eq` 📖	mathematical	—	`Equiv.symm` `Topology.WithScott` `ofScott` `toScott`	—	—
`ofScott_toScott` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithScott` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofScott` `toScott`	—	—
`toScott_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithScott` `EquivLike.toFunLike` `Equiv.instEquivLike` `toScott`	—	—
`toScott_ofScott` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Topology.WithScott` `EquivLike.toFunLike` `Equiv.instEquivLike` `toScott` `ofScott`	—	—
`toScott_symm_eq` 📖	mathematical	—	`Equiv.symm` `Topology.WithScott` `toScott` `ofScott`	—	—

---

← Back to Index