let M, N be complete LATTICE; 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; 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; ( InclPoset (sigma N) is continuous implies the topology of [:LM,LN:] = lambda [:M,N:] )
assume A1:
InclPoset (sigma N) is continuous
; the topology of [:LM,LN:] = lambda [:M,N:]
consider SMN being non empty correct Scott TopAugmentation of [:M,N:];
consider lMN being non empty correct lower TopAugmentation of [:M,N:];
consider LMN being non empty correct Lawson TopAugmentation of [:M,N:];
A2:
[:LM,LN:] = TopStruct(# the carrier of LMN, the topology of LMN #)
proof
consider lN being non
empty correct lower TopAugmentation of
N;
consider lM being non
empty correct lower TopAugmentation of
M;
consider SN being non
empty correct Scott TopAugmentation of
N;
consider SM being non
empty correct Scott TopAugmentation of
M;
A3:
LN is
Refinement of
SN,
lN
by WAYBEL19:29;
A4:
RelStr(# the
carrier of
lN, the
InternalRel of
lN #)
= RelStr(# the
carrier of
N, the
InternalRel of
N #)
by YELLOW_9:def 4;
(omega LMN) \/ (sigma LMN) is
prebasis of
LMN
by WAYBEL19:def 3;
then A5:
(omega LMN) \/ (sigma LMN) is
prebasis of
TopStruct(# the
carrier of
LMN, the
topology of
LMN #)
by YELLOW12:33;
A6:
RelStr(# the
carrier of
LM, the
InternalRel of
LM #)
= RelStr(# the
carrier of
M, the
InternalRel of
M #)
by YELLOW_9:def 4;
A7:
RelStr(# the
carrier of
LN, the
InternalRel of
LN #)
= RelStr(# the
carrier of
N, the
InternalRel of
N #)
by YELLOW_9:def 4;
A8:
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;
A9: the
carrier of
[:LM,LN:] =
[: the carrier of LM, the carrier of LN:]
by BORSUK_1:def 5
.=
the
carrier of
LMN
by A6, A7, A8, YELLOW_3:def 2
;
A10: the
topology of
[:lM,lN:] =
omega [:M,N:]
by WAYBEL19:15
.=
omega LMN
by A8, WAYBEL19:3
;
A11:
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
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 A12:
TopStruct(# the
carrier of
SM, the
topology of
SM #)
= TopStruct(# the
carrier of
(Sigma M), the
topology of
(Sigma M) #)
by WAYBEL29:17;
A13:
RelStr(# the
carrier of
lM, the
InternalRel of
lM #)
= RelStr(# the
carrier of
M, the
InternalRel of
M #)
by YELLOW_9:def 4;
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
;
then
TopStruct(# the
carrier of
SN, the
topology of
SN #)
= TopStruct(# the
carrier of
(Sigma N), the
topology of
(Sigma N) #)
by WAYBEL29:17;
then A14: the
topology of
[:SM,SN:] =
the
topology of
[:(Sigma M),(Sigma N):]
by A12, WAYBEL29:10
.=
sigma [:M,N:]
by A1, WAYBEL29:34
.=
sigma LMN
by A8, YELLOW_9:52
;
A15:
RelStr(# the
carrier of
SM, the
InternalRel of
SM #)
= RelStr(# the
carrier of
M, the
InternalRel of
M #)
by YELLOW_9:def 4;
A16:
LM is
Refinement of
SM,
lM
by WAYBEL19:29;
then
[:LM,LN:] is
Refinement of
[:SM,SN:],
[:lM,lN:]
by A3, A15, A11, A13, A4, YELLOW12:50;
then
the
carrier of
TopStruct(# the
carrier of
LMN, the
topology of
LMN #)
= the
carrier of
[:SM,SN:] \/ the
carrier of
[:lM,lN:]
by A9, YELLOW_9:def 6;
then
TopStruct(# the
carrier of
LMN, the
topology of
LMN #) is
Refinement of
[:SM,SN:],
[:lM,lN:]
by A5, YELLOW_9:def 6, A14, A10;
hence
[:LM,LN:] = TopStruct(# the
carrier of
LMN, the
topology of
LMN #)
by A16, A3, A15, A11, A13, A4, A9, YELLOW12:49;
verum
end;
LMN is Refinement of SMN,lMN
by WAYBEL19:29;
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; verum