begin
theorem
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
:: deftheorem Def1 defines is_Retract_of WAYBEL25:def 1 :
for X, Y being non empty TopSpace holds
( X is_Retract_of Y iff ex c being continuous Function of X,Y ex r being continuous Function of Y,X st r * c = id X );
theorem
theorem
theorem
theorem
theorem Th12:
begin
definition
let T be
TopStruct ;
func Omega T -> strict TopRelStr means :
Def2:
(
TopStruct(# the
carrier of
it,the
topology of
it #)
= TopStruct(# the
carrier of
T,the
topology of
T #) & ( for
x,
y being
Element of
it holds
(
x <= y iff ex
Y being
Subset of
T st
(
Y = {y} &
x in Cl Y ) ) ) );
existence
ex b1 being strict TopRelStr st
( TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of T,the topology of T #) & ( for x, y being Element of b1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) )
uniqueness
for b1, b2 being strict TopRelStr st TopStruct(# the carrier of b1,the topology of b1 #) = TopStruct(# the carrier of T,the topology of T #) & ( for x, y being Element of b1 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) & TopStruct(# the carrier of b2,the topology of b2 #) = TopStruct(# the carrier of T,the topology of T #) & ( for x, y being Element of b2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines Omega WAYBEL25:def 2 :
for T being TopStruct
for b2 being strict TopRelStr holds
( b2 = Omega T iff ( TopStruct(# the carrier of b2,the topology of b2 #) = TopStruct(# the carrier of T,the topology of T #) & ( for x, y being Element of b2 holds
( x <= y iff ex Y being Subset of T st
( Y = {y} & x in Cl Y ) ) ) ) );
Lm1:
for T being TopStruct holds the carrier of T = the carrier of (Omega T)
Lm2:
for T being TopStruct
for x, y being Element of T
for X, Y being Subset of T st X = {x} & Y = {y} holds
( x in Cl Y iff Cl X c= Cl Y )
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
Lm3:
for S, T being non empty RelStr
for f being Function of S,S
for g being Function of T,T st RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) & f = g & f is projection holds
g is projection
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
Lm4:
now
let X,
Y be non
empty TopSpace;
for N being net of ContMaps X,(Omega Y) holds the mapping of N in Funcs the carrier of N,(Funcs the carrier of X,the carrier of Y)let N be
net of
ContMaps X,
(Omega Y);
the mapping of N in Funcs the carrier of N,(Funcs the carrier of X,the carrier of Y)A1:
the
carrier of
Y = the
carrier of
(Omega Y)
by Lm1;
the
carrier of
(ContMaps X,(Omega Y)) c= Funcs the
carrier of
X,the
carrier of
Y
then A2:
Funcs the
carrier of
N,the
carrier of
(ContMaps X,(Omega Y)) c= Funcs the
carrier of
N,
(Funcs the carrier of X,the carrier of Y)
by FUNCT_5:63;
the
mapping of
N in Funcs the
carrier of
N,the
carrier of
(ContMaps X,(Omega Y))
by FUNCT_2:11;
hence
the
mapping of
N in Funcs the
carrier of
N,
(Funcs the carrier of X,the carrier of Y)
by A2;
verum
end;
definition
let I be non
empty set ;
let S,
T be non
empty RelStr ;
let N be
net of
T;
let i be
Element of
I;
assume A1:
the
carrier of
T c= the
carrier of
(S |^ I)
;
func commute N,
i,
S -> strict net of
S means :
Def3:
(
RelStr(# the
carrier of
it,the
InternalRel of
it #)
= RelStr(# the
carrier of
N,the
InternalRel of
N #) & the
mapping of
it = (commute the mapping of N) . i );
existence
ex b1 being strict net of S st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b1 = (commute the mapping of N) . i )
uniqueness
for b1, b2 being strict net of S st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b1 = (commute the mapping of N) . i & RelStr(# the carrier of b2,the InternalRel of b2 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b2 = (commute the mapping of N) . i holds
b1 = b2
;
end;
:: deftheorem Def3 defines commute WAYBEL25:def 3 :
for I being non empty set
for S, T being non empty RelStr
for N being net of T
for i being Element of I st the carrier of T c= the carrier of (S |^ I) holds
for b6 being strict net of S holds
( b6 = commute N,i,S iff ( RelStr(# the carrier of b6,the InternalRel of b6 #) = RelStr(# the carrier of N,the InternalRel of N #) & the mapping of b6 = (commute the mapping of N) . i ) );
theorem Th24:
theorem Th25:
Lm5:
now
let X,
Y be non
empty TopSpace;
for N being net of ContMaps X,(Omega Y)
for i being Element of N holds
( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )let N be
net of
ContMaps X,
(Omega Y);
for i being Element of N holds
( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )let i be
Element of
N;
( the mapping of N . i is Function of X,(Omega Y) & the mapping of N . i is Function of X,Y )thus
the
mapping of
N . i is
Function of
X,
(Omega Y)
by WAYBEL24:21;
the mapping of N . i is Function of X,Y
the
carrier of
Y = the
carrier of
(Omega Y)
by Lm1;
hence
the
mapping of
N . i is
Function of
X,
Y
by WAYBEL24:21;
verum
end;
Lm6:
now
let X,
Y be non
empty TopSpace;
for N being net of ContMaps X,(Omega Y)
for x being Point of X holds dom the mapping of N = dom the mapping of (commute N,x,(Omega Y))let N be
net of
ContMaps X,
(Omega Y);
for x being Point of X holds dom the mapping of N = dom the mapping of (commute N,x,(Omega Y))let x be
Point of
X;
dom the mapping of N = dom the mapping of (commute N,x,(Omega Y))
ContMaps X,
(Omega Y) is
SubRelStr of
(Omega Y) |^ the
carrier of
X
by WAYBEL24:def 3;
then
the
carrier of
(ContMaps X,(Omega Y)) c= the
carrier of
((Omega Y) |^ the carrier of X)
by YELLOW_0:def 13;
then A1:
RelStr(# the
carrier of
N,the
InternalRel of
N #)
= RelStr(# the
carrier of
(commute N,x,(Omega Y)),the
InternalRel of
(commute N,x,(Omega Y)) #)
by Def3;
thus dom the
mapping of
N =
the
carrier of
N
by FUNCT_2:def 1
.=
dom the
mapping of
(commute N,x,(Omega Y))
by A1, FUNCT_2:def 1
;
verum
end;
theorem Th26:
begin
:: deftheorem Def4 defines monotone-convergence WAYBEL25:def 4 :
for T being non empty TopSpace holds
( T is monotone-convergence iff for D being non empty directed Subset of (Omega T) holds
( ex_sup_of D, Omega T & ( for V being open Subset of T st sup D in V holds
D meets V ) ) );
theorem Th27:
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem