:: Continuous Lattices between T$_0$ Spaces
:: by Grzegorz Bancerek
::
:: Received September 24, 1999
:: Copyright (c) 1999 Association of Mizar Users
:: deftheorem defines oContMaps WAYBEL26:def 1 :
theorem Th1: :: WAYBEL26:1
theorem Th2: :: WAYBEL26:2
theorem Th3: :: WAYBEL26:3
theorem Th4: :: WAYBEL26:4
theorem Th5: :: WAYBEL26:5
theorem Th6: :: WAYBEL26:6
definition
let X,
Y,
Z be non
empty TopSpace;
let f be
continuous Function of
Y,
Z;
func oContMaps X,
f -> Function of
(oContMaps X,Y),
(oContMaps X,Z) means :
Def2:
:: WAYBEL26:def 2
for
g being
continuous Function of
X,
Y holds
it . g = f * g;
uniqueness
for b1, b2 being Function of (oContMaps X,Y),(oContMaps X,Z) st ( for g being continuous Function of X,Y holds b1 . g = f * g ) & ( for g being continuous Function of X,Y holds b2 . g = f * g ) holds
b1 = b2
existence
ex b1 being Function of (oContMaps X,Y),(oContMaps X,Z) st
for g being continuous Function of X,Y holds b1 . g = f * g
func oContMaps f,
X -> Function of
(oContMaps Z,X),
(oContMaps Y,X) means :
Def3:
:: WAYBEL26:def 3
for
g being
continuous Function of
Z,
X holds
it . g = g * f;
uniqueness
for b1, b2 being Function of (oContMaps Z,X),(oContMaps Y,X) st ( for g being continuous Function of Z,X holds b1 . g = g * f ) & ( for g being continuous Function of Z,X holds b2 . g = g * f ) holds
b1 = b2
existence
ex b1 being Function of (oContMaps Z,X),(oContMaps Y,X) st
for g being continuous Function of Z,X holds b1 . g = g * f
end;
:: deftheorem Def2 defines oContMaps WAYBEL26:def 2 :
:: deftheorem Def3 defines oContMaps WAYBEL26:def 3 :
theorem :: WAYBEL26:7
canceled;
theorem Th8: :: WAYBEL26:8
theorem Th9: :: WAYBEL26:9
theorem :: WAYBEL26:10
theorem Th11: :: WAYBEL26:11
theorem Th12: :: WAYBEL26:12
theorem Th13: :: WAYBEL26:13
theorem Th14: :: WAYBEL26:14
theorem Th15: :: WAYBEL26:15
theorem Th16: :: WAYBEL26:16
theorem Th17: :: WAYBEL26:17
theorem Th18: :: WAYBEL26:18
Lm1:
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
Y is monotone-convergence
theorem Th19: :: WAYBEL26:19
theorem Th20: :: WAYBEL26:20
theorem Th21: :: WAYBEL26:21
theorem Th22: :: WAYBEL26:22
theorem Th23: :: WAYBEL26:23
theorem Th24: :: WAYBEL26:24
theorem Th25: :: WAYBEL26:25
theorem Th26: :: WAYBEL26:26
theorem Th27: :: WAYBEL26:27
theorem Th28: :: WAYBEL26:28
theorem Th29: :: WAYBEL26:29
theorem Th30: :: WAYBEL26:30
theorem Th31: :: WAYBEL26:31
theorem Th32: :: WAYBEL26:32
theorem Th33: :: WAYBEL26:33
theorem Th34: :: WAYBEL26:34
theorem Th35: :: WAYBEL26:35
theorem Th36: :: WAYBEL26:36
theorem Th37: :: WAYBEL26:37
theorem :: WAYBEL26:38
:: deftheorem defines *graph WAYBEL26:def 4 :
theorem Th39: :: WAYBEL26:39
theorem Th40: :: WAYBEL26:40
theorem Th41: :: WAYBEL26:41
:: deftheorem Def5 defines *graph WAYBEL26:def 5 :
theorem Th42: :: WAYBEL26:42
theorem Th43: :: WAYBEL26:43
theorem Th44: :: WAYBEL26:44
theorem Th45: :: WAYBEL26:45
theorem :: WAYBEL26:46