ScottTopology

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

Statistics

Metric	Count
Definitions DirSupClosed, DirSupInacc, DirSupInaccOn, IsScott, withScottHomeomorph, IsScottHausdorff, WithScott, instInhabited, instPreorder, instTopologicalSpace, ofScott, rec, toScott, scott, scottHausdorff	15
Theorems compl, inter, of_compl, compl, dirSupInaccOn, of_compl, union, mono, dirSupInacc, dirSupClosed, 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_of_isUpperSet, isOpen_iff, 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, dirSupClosed_Iic, dirSupClosed_compl, dirSupClosed_iff_forall_sSup, dirSupInaccOn_univ, dirSupInacc_compl, dirSupInacc_iff_forall_sSup	56
Total	71

DirSupClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl 📖	mathematical	DirSupClosed	DirSupInacc Compl.compl Set Set.instCompl	—	dirSupInacc_compl
inter 📖	mathematical	DirSupClosed	Set Set.instInter	—	HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_left Set.inter_subset_right
of_compl 📖	mathematical	DirSupClosed Compl.compl Set Set.instCompl	DirSupInacc	—	dirSupClosed_compl

DirSupInacc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl 📖	mathematical	DirSupInacc	DirSupClosed Compl.compl Set Set.instCompl	—	dirSupClosed_compl
dirSupInaccOn 📖	mathematical	DirSupInacc	DirSupInaccOn	—	—
of_compl 📖	mathematical	DirSupInacc Compl.compl Set Set.instCompl	DirSupClosed	—	dirSupInacc_compl
union 📖	mathematical	DirSupInacc	Set Set.instUnion	—	dirSupClosed_compl Set.compl_union DirSupClosed.inter compl

DirSupInaccOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	Set Set.instHasSubset DirSupInaccOn	—	—	—

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dirSupInacc 📖	mathematical	IsLowerSet Preorder.toLE	DirSupInacc	—	DirSupClosed.of_compl IsUpperSet.dirSupClosed compl

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dirSupClosed 📖	mathematical	IsUpperSet Preorder.toLE	DirSupClosed	—	—

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_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_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	—	—

(root)

Definitions

Name	Category	Theorems
DirSupClosed 📖	MathDef	11 math math: dirSupClosed_iff_forall_sSup, Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed, IsUpperSet.dirSupClosed, dirSupClosed_Iic, dirSupInacc_compl, DirSupInacc.of_compl, Topology.lawsonClosed_iff_dirSupClosed_of_isLowerSet, dirSupClosed_compl, Topology.IsScottHausdorff.dirSupClosed_of_isClosed, DirSupInacc.compl, Topology.IsScott.dirSupClosed_of_isClosed
DirSupInacc 📖	MathDef	7 math math: DirSupClosed.of_compl, DirSupClosed.compl, dirSupInacc_compl, dirSupInaccOn_univ, dirSupClosed_compl, IsLowerSet.dirSupInacc, dirSupInacc_iff_forall_sSup
DirSupInaccOn 📖	MathDef	4 math math: Topology.IsScottHausdorff.dirSupInaccOn_of_isOpen, dirSupInaccOn_univ, Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn, DirSupInacc.dirSupInaccOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dirSupClosed_Iic 📖	mathematical	—	DirSupClosed Set.Iic	—	isLUB_le_iff
dirSupClosed_compl 📖	mathematical	—	DirSupClosed Compl.compl Set Set.instCompl DirSupInacc	—	dirSupInacc_compl compl_compl
dirSupClosed_iff_forall_sSup 📖	mathematical	—	DirSupClosed PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Set Set.instMembership SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	—
dirSupInaccOn_univ 📖	mathematical	—	DirSupInaccOn Set.univ Set DirSupInacc	—	—
dirSupInacc_compl 📖	mathematical	—	DirSupInacc Compl.compl Set Set.instCompl DirSupClosed	—	—
dirSupInacc_iff_forall_sSup 📖	mathematical	—	DirSupInacc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Set.Nonempty Set Set.instInter	—	—

---

← Back to Index