let M, N be complete LATTICE; :: thesis: for LM being correct Lawson TopAugmentation of M
for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
the topology of [:LM,LN:] = lambda [:M,N:]
let LM be correct Lawson TopAugmentation of M; :: thesis: for LN being correct Lawson TopAugmentation of N st InclPoset (sigma N) is continuous holds
the topology of [:LM,LN:] = lambda [:M,N:]
let LN be correct Lawson TopAugmentation of N; :: thesis: ( InclPoset (sigma N) is continuous implies the topology of [:LM,LN:] = lambda [:M,N:] )
assume A1:
InclPoset (sigma N) is continuous
; :: thesis: the topology of [:LM,LN:] = lambda [:M,N:]
consider LMN being non empty correct Lawson TopAugmentation of [:M,N:];
consider lMN being non empty correct lower TopAugmentation of [:M,N:];
consider SMN being non empty correct Scott TopAugmentation of [:M,N:];
A2:
LMN is Refinement of SMN,lMN
by WAYBEL19:29;
[:LM,LN:] = TopStruct(# the carrier of LMN,the topology of LMN #)
proof
consider SM being non
empty correct Scott TopAugmentation of
M;
consider SN being non
empty correct Scott TopAugmentation of
N;
consider lM being non
empty correct lower TopAugmentation of
M;
consider lN being non
empty correct lower TopAugmentation of
N;
A3:
(
LM is
Refinement of
SM,
lM &
LN is
Refinement of
SN,
lN )
by WAYBEL19:29;
A4:
(
RelStr(# the
carrier of
SM,the
InternalRel of
SM #)
= RelStr(# the
carrier of
M,the
InternalRel of
M #) &
RelStr(# the
carrier of
SN,the
InternalRel of
SN #)
= RelStr(# the
carrier of
N,the
InternalRel of
N #) &
RelStr(# the
carrier of
lM,the
InternalRel of
lM #)
= RelStr(# the
carrier of
M,the
InternalRel of
M #) &
RelStr(# the
carrier of
lN,the
InternalRel of
lN #)
= RelStr(# the
carrier of
N,the
InternalRel of
N #) )
by YELLOW_9:def 4;
A5:
(
RelStr(# the
carrier of
LM,the
InternalRel of
LM #)
= RelStr(# the
carrier of
M,the
InternalRel of
M #) &
RelStr(# the
carrier of
LN,the
InternalRel of
LN #)
= RelStr(# the
carrier of
N,the
InternalRel of
N #) )
by YELLOW_9:def 4;
A6:
RelStr(# the
carrier of
LMN,the
InternalRel of
LMN #)
= RelStr(# the
carrier of
[:M,N:],the
InternalRel of
[:M,N:] #)
by YELLOW_9:def 4;
A7: the
carrier of
[:LM,LN:] =
[:the carrier of LM,the carrier of LN:]
by BORSUK_1:def 5
.=
the
carrier of
LMN
by A5, A6, YELLOW_3:def 2
;
TopStruct(# the
carrier of
LMN,the
topology of
LMN #) is
Refinement of
[:SM,SN:],
[:lM,lN:]
proof
[:LM,LN:] is
Refinement of
[:SM,SN:],
[:lM,lN:]
by A3, A4, YELLOW12:50;
hence
the
carrier of
TopStruct(# the
carrier of
LMN,the
topology of
LMN #)
= the
carrier of
[:SM,SN:] \/ the
carrier of
[:lM,lN:]
by A7, YELLOW_9:def 6;
:: according to YELLOW_9:def 6 :: thesis: the topology of [:SM,SN:] \/ the topology of [:lM,lN:] is prebasis of TopStruct(# the carrier of LMN,the topology of LMN #)
A8:
(omega LMN) \/ (sigma LMN) is
prebasis of
LMN
by WAYBEL19:def 3;
A9: the
topology of
[:lM,lN:] =
omega [:M,N:]
by WAYBEL19:15
.=
omega LMN
by A6, WAYBEL19:3
;
A10:
RelStr(# the
carrier of
SN,the
InternalRel of
SN #) =
RelStr(# the
carrier of
N,the
InternalRel of
N #)
by YELLOW_9:def 4
.=
RelStr(# the
carrier of
(Sigma N),the
InternalRel of
(Sigma N) #)
by YELLOW_9:def 4
;
RelStr(# the
carrier of
SM,the
InternalRel of
SM #) =
RelStr(# the
carrier of
M,the
InternalRel of
M #)
by YELLOW_9:def 4
.=
RelStr(# the
carrier of
(Sigma M),the
InternalRel of
(Sigma M) #)
by YELLOW_9:def 4
;
then
(
TopStruct(# the
carrier of
SN,the
topology of
SN #)
= TopStruct(# the
carrier of
(Sigma N),the
topology of
(Sigma N) #) &
TopStruct(# the
carrier of
SM,the
topology of
SM #)
= TopStruct(# the
carrier of
(Sigma M),the
topology of
(Sigma M) #) )
by A10, WAYBEL29:17;
then the
topology of
[:SM,SN:] =
the
topology of
[:(Sigma M),(Sigma N):]
by WAYBEL29:10
.=
sigma [:M,N:]
by A1, WAYBEL29:34
.=
sigma LMN
by A6, YELLOW_9:52
;
hence
the
topology of
[:SM,SN:] \/ the
topology of
[:lM,lN:] is
prebasis of
TopStruct(# the
carrier of
LMN,the
topology of
LMN #)
by A8, A9, YELLOW12:33;
:: thesis: verum
end;
hence
[:LM,LN:] = TopStruct(# the
carrier of
LMN,the
topology of
LMN #)
by A3, A4, A7, YELLOW12:49;
:: thesis: verum
end;
then reconsider R = [:LM,LN:] as Refinement of SMN,lMN by A2, YELLOW12:47;
the topology of [:LM,LN:] = the topology of R
;
hence
the topology of [:LM,LN:] = lambda [:M,N:]
by WAYBEL19:34; :: thesis: verum