begin
:: deftheorem defines oContMaps WAYBEL26:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
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:
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:
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
canceled;
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
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:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem
:: deftheorem defines *graph WAYBEL26:def 4 :
theorem Th39:
theorem Th40:
theorem Th41:
:: deftheorem Def5 defines *graph WAYBEL26:def 5 :
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem