:: Scott-Continuous Functions, Part II
:: by Adam Grabowski
::
:: Received June 22, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: WAYBEL24:1
theorem :: WAYBEL24:2
theorem :: WAYBEL24:3
theorem Th4: :: WAYBEL24:4
theorem :: WAYBEL24:5
theorem Th6: :: WAYBEL24:6
:: deftheorem defines Proj WAYBEL24:def 1 :
theorem Th7: :: WAYBEL24:7
:: deftheorem defines Proj WAYBEL24:def 2 :
theorem Th8: :: WAYBEL24:8
theorem Th9: :: WAYBEL24:9
theorem Th10: :: WAYBEL24:10
theorem Th11: :: WAYBEL24:11
theorem Th12: :: WAYBEL24:12
theorem :: WAYBEL24:13
theorem Th14: :: WAYBEL24:14
theorem Th15: :: WAYBEL24:15
theorem :: WAYBEL24:16
theorem Th17: :: WAYBEL24:17
theorem :: WAYBEL24:18
theorem Th19: :: WAYBEL24:19
:: deftheorem Def3 defines ContMaps WAYBEL24:def 3 :
theorem Th20: :: WAYBEL24:20
theorem Th21: :: WAYBEL24:21
theorem :: WAYBEL24:22
theorem Th23: :: WAYBEL24:23
theorem :: WAYBEL24:24
theorem Th25: :: WAYBEL24:25
theorem Th26: :: WAYBEL24:26
theorem Th27: :: WAYBEL24:27
theorem Th28: :: WAYBEL24:28
Lm1:
for S being non empty RelStr
for D being non empty Subset of S holds D = { i where i is Element of S : i in D }
theorem Th29: :: WAYBEL24:29
theorem Th30: :: WAYBEL24:30
theorem Th31: :: WAYBEL24:31
theorem Th32: :: WAYBEL24:32
theorem Th33: :: WAYBEL24:33
theorem :: WAYBEL24:34
theorem Th35: :: WAYBEL24:35
theorem :: WAYBEL24:36
theorem :: WAYBEL24:37
theorem :: WAYBEL24:38