begin
theorem
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
:: deftheorem Def1 defines is_Retract_of WAYBEL25:def 1 :
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 holds
(
x <= y iff ex
Y being
Subset of 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 holds
( x <= y iff ex Y being Subset of 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 holds
( x <= y iff ex Y being Subset of 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 holds
( x <= y iff ex Y being Subset of st
( Y = {y} & x in Cl Y ) ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines Omega WAYBEL25:def 2 :
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
for X, Y being Subset of 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 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 ;
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 ;
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
strict 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 strict 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 strict 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 :
theorem Th24:
theorem Th25:
Lm5:
now
let X,
Y be non
empty TopSpace;
for N being net of Function-yielding
for i being Element of 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
Function-yielding ;
for i being Element of 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 ;
( 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 Function-yielding
for x being Point of holds dom the mapping of N = dom the mapping of (commute N,x,(Omega Y))let N be
net of
Function-yielding ;
for x being Point of holds dom the mapping of N = dom the mapping of (commute N,x,(Omega Y))let x be
Point of ;
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 :
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