:: The Scott Topology, Part II
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received August 27, 1997
:: Copyright (c) 1997 Association of Mizar Users
theorem Th1: :: WAYBEL14:1
Lm1:
for S being 1-sorted
for X, Y being Subset of S holds
( X c= Y ` iff Y c= X ` )
theorem Th2: :: WAYBEL14:2
theorem Th3: :: WAYBEL14:3
theorem :: WAYBEL14:4
theorem Th5: :: WAYBEL14:5
theorem :: WAYBEL14:6
theorem Th7: :: WAYBEL14:7
theorem :: WAYBEL14:8
theorem Th9: :: WAYBEL14:9
theorem Th10: :: WAYBEL14:10
theorem :: WAYBEL14:11
theorem Th12: :: WAYBEL14:12
theorem :: WAYBEL14:13
theorem Th14: :: WAYBEL14:14
theorem Th15: :: WAYBEL14:15
theorem :: WAYBEL14:16
theorem Th17: :: WAYBEL14:17
theorem Th18: :: WAYBEL14:18
theorem Th19: :: WAYBEL14:19
theorem :: WAYBEL14:20
theorem Th21: :: WAYBEL14:21
theorem Th22: :: WAYBEL14:22
theorem Th23: :: WAYBEL14:23
theorem Th24: :: WAYBEL14:24
Lm2:
for L being complete Scott TopLattice
for V being filtered Subset of L
for F being Subset-Family of L
for CF being Subset of (InclPoset (sigma L)) st F = { (downarrow u) where u is Element of L : u in V } & CF = COMPLEMENT F holds
CF is directed
theorem Th25: :: WAYBEL14:25
theorem Th26: :: WAYBEL14:26
:: deftheorem Def1 defines jointly_Scott-continuous WAYBEL14:def 1 :
theorem Th27: :: WAYBEL14:27
theorem :: WAYBEL14:28
theorem Th29: :: WAYBEL14:29
theorem Th30: :: WAYBEL14:30
theorem Th31: :: WAYBEL14:31
theorem :: WAYBEL14:32
theorem Th33: :: WAYBEL14:33
theorem :: WAYBEL14:34
theorem :: WAYBEL14:35
theorem :: WAYBEL14:36
theorem Th37: :: WAYBEL14:37
theorem Th38: :: WAYBEL14:38
theorem Th39: :: WAYBEL14:39
theorem :: WAYBEL14:40
theorem :: WAYBEL14:41
theorem :: WAYBEL14:42
theorem :: WAYBEL14:43
theorem :: WAYBEL14:44
theorem :: WAYBEL14:45