OmegaCompletePartialOrder

📁 Source: Mathlib/Topology/OmegaCompletePartialOrder.lean

Statistics

Metric	Count
Definitions OmegaCompletePartialOrder, IsOpen, IsωSup	3
Theorems inter, isUpperSet, isOpen_sUnion, isOpen_univ, isωSup_iff_isLUB, ωScottContinuous_iff_continuous, isωSup_ωSup	7
Total	10

Scott

Definitions

Name	Category	Theorems
IsOpen 📖	MathDef	1 math math: isOpen_univ
IsωSup 📖	MathDef	2 math math: isωSup_ωSup, isωSup_iff_isLUB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpen_sUnion 📖	mathematical	IsOpen	Set.sUnion	—	iSup_Prop_eq CompleteLattice.ωScottContinuous.sSup
isOpen_univ 📖	mathematical	—	IsOpen Set.univ	—	CompleteLattice.ωScottContinuous.top
isωSup_iff_isLUB 📖	mathematical	—	IsωSup IsLUB Preorder.toLE Set.range DFunLike.coe OmegaCompletePartialOrder.Chain OmegaCompletePartialOrder.Chain.instFunLikeNat	—	—

Scott.IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter 📖	mathematical	Scott.IsOpen	Set Set.instInter	—	CompleteLattice.ωScottContinuous.inf
isUpperSet 📖	mathematical	Scott.IsOpen	IsUpperSet Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder	—	OmegaCompletePartialOrder.ωScottContinuous.monotone

Topology.IsScott

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ωScottContinuous_iff_continuous 📖	mathematical	—	OmegaCompletePartialOrder.ωScottContinuous CompleteLattice.instOmegaCompletePartialOrder Prop.instCompleteLattice Continuous sierpinskiSpace	—	OmegaCompletePartialOrder.ωScottContinuous.eq_1 scottContinuousOn_iff_continuous instUnivSetOfIsUpper instIsUpperProp OmegaCompletePartialOrder.Chain.range_pair

(root)

Definitions

Name	Category	Theorems
OmegaCompletePartialOrder 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isωSup_ωSup 📖	mathematical	—	Scott.IsωSup PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder OmegaCompletePartialOrder.ωSup	—	OmegaCompletePartialOrder.le_ωSup OmegaCompletePartialOrder.ωSup_le

---

← Back to Index