let N be complete Lawson meet-continuous TopLattice; ( InclPoset (sigma N) is continuous implies ( N is Hausdorff iff for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed ) )
assume A1:
InclPoset (sigma N) is continuous
; ( N is Hausdorff iff for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed )
A2:
[: the carrier of N, the carrier of N:] = the carrier of [:N,N:]
by BORSUK_1:def 2;
hereby ( ( for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed ) implies N is Hausdorff )
reconsider D =
id the
carrier of
N as
Subset of
[:N,N:] by BORSUK_1:def 2;
set INF =
inf_op N;
set f =
<:(pr1 ( the carrier of N, the carrier of N)),(inf_op N):>;
assume
N is
Hausdorff
;
for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed then A3:
D is
closed
by YELLOW12:46;
A4:
the
carrier of
[:N,N:] = [: the carrier of N, the carrier of N:]
by YELLOW_3:def 2;
then reconsider f =
<:(pr1 ( the carrier of N, the carrier of N)),(inf_op N):> as
Function of
[:N,N:],
[:N,N:] by A2, FUNCT_3:58;
let X be
Subset of
[:N,N:];
( X = the InternalRel of N implies X is closed )assume A5:
X = the
InternalRel of
N
;
X is closed A6:
for
x,
y being
Element of
N holds
f . [x,y] = [x,(x "/\" y)]
proof
let x,
y be
Element of
N;
f . [x,y] = [x,(x "/\" y)]
A7:
dom (pr1 ( the carrier of N, the carrier of N)) = [: the carrier of N, the carrier of N:]
by FUNCT_2:def 1;
A8:
[x,y] in [: the carrier of N, the carrier of N:]
by ZFMISC_1:87;
dom (inf_op N) = [: the carrier of N, the carrier of N:]
by A4, FUNCT_2:def 1;
hence f . [x,y] =
[((pr1 ( the carrier of N, the carrier of N)) . (x,y)),((inf_op N) . (x,y))]
by A8, A7, FUNCT_3:49
.=
[x,((inf_op N) . (x,y))]
by FUNCT_3:def 4
.=
[x,(x "/\" y)]
by WAYBEL_2:def 4
;
verum
end; A9:
X = f " D
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 f " D c= X
let a be
object ;
( a in X implies a in f " D )assume A10:
a in X
;
a in f " Dthen consider s,
t being
object such that A11:
s in the
carrier of
N
and A12:
t in the
carrier of
N
and A13:
a = [s,t]
by A5, ZFMISC_1:def 2;
reconsider s =
s,
t =
t as
Element of
N by A11, A12;
s <= t
by A5, A10, A13, ORDERS_2:def 5;
then
s "/\" t = s
by YELLOW_0:25;
then
f . [s,t] = [s,s]
by A6;
then A14:
f . a in D
by A13, RELAT_1:def 10;
dom f = the
carrier of
[:N,N:]
by FUNCT_2:def 1;
then
a in dom f
by A2, A11, A12, A13, ZFMISC_1:87;
hence
a in f " D
by A14, FUNCT_1:def 7;
verum
end;
let a be
object ;
TARSKI:def 3 ( not a in f " D or a in X )
assume A15:
a in f " D
;
a in X
then A16:
f . a in D
by FUNCT_1:def 7;
consider s,
t being
object such that A17:
s in the
carrier of
N
and A18:
t in the
carrier of
N
and A19:
a = [s,t]
by A2, A15, ZFMISC_1:def 2;
reconsider s =
s,
t =
t as
Element of
N by A17, A18;
f . a = [s,(s "/\" t)]
by A6, A19;
then
s = s "/\" t
by A16, RELAT_1:def 10;
then
s <= t
by YELLOW_0:25;
hence
a in X
by A5, A19, ORDERS_2:def 5;
verum
end; reconsider INF =
inf_op N as
Function of
[:N,N:],
N by A2, A4;
N is
topological_semilattice
by A1, Th22;
then A20:
INF is
continuous
;
pr1 ( the
carrier of
N, the
carrier of
N) is
continuous Function of
[:N,N:],
N
by YELLOW12:39;
then
f is
continuous
by A20, YELLOW12:41;
hence
X is
closed
by A9, A3;
verum
end;
assume A21:
for X being Subset of [:N,N:] st X = the InternalRel of N holds
X is closed
; N is Hausdorff
A22:
the InternalRel of N /\ the InternalRel of (N ~) c= id the carrier of N
by YELLOW12:23;
id the carrier of N c= the InternalRel of N /\ the InternalRel of (N ~)
by YELLOW12:22;
then A23:
id the carrier of N = the InternalRel of N /\ the InternalRel of (N ~)
by A22;
for A being Subset of [:N,N:] st A = id the carrier of N holds
A is closed
proof
reconsider f =
<:(pr2 ( the carrier of N, the carrier of N)),(pr1 ( the carrier of N, the carrier of N)):> as
continuous Function of
[:N,N:],
[:N,N:] by YELLOW12:42;
reconsider X = the
InternalRel of
N,
Y = the
InternalRel of
(N ~) as
Subset of
[:N,N:] by BORSUK_1:def 2;
let A be
Subset of
[:N,N:];
( A = id the carrier of N implies A is closed )
assume A24:
A = id the
carrier of
N
;
A is closed
reconsider X =
X,
Y =
Y as
Subset of
[:N,N:] ;
A25:
X is
closed
by A21;
A26:
dom f = [: the carrier of N, the carrier of N:]
by YELLOW12:4;
A27:
f .: X = Y
proof
thus
f .: X c= Y
XBOOLE_0:def 10 Y c= f .: Xproof
let y be
object ;
TARSKI:def 3 ( not y in f .: X or y in Y )
assume
y in f .: X
;
y in Y
then consider x being
object such that
x in dom f
and A28:
x in X
and A29:
y = f . x
by FUNCT_1:def 6;
consider x1,
x2 being
object such that A30:
x1 in the
carrier of
N
and A31:
x2 in the
carrier of
N
and A32:
x = [x1,x2]
by A28, ZFMISC_1:def 2;
f . x = [x2,x1]
by A30, A31, A32, Lm3;
hence
y in Y
by A28, A29, A32, RELAT_1:def 7;
verum
end;
let y be
object ;
TARSKI:def 3 ( not y in Y or y in f .: X )
assume A33:
y in Y
;
y in f .: X
then consider y1,
y2 being
object such that A34:
y1 in the
carrier of
N
and A35:
y2 in the
carrier of
N
and A36:
y = [y1,y2]
by ZFMISC_1:def 2;
A37:
[y2,y1] in X
by A33, A36, RELAT_1:def 7;
f . [y2,y1] = y
by A34, A35, A36, Lm3;
hence
y in f .: X
by A26, A37, FUNCT_1:def 6;
verum
end;
f is
being_homeomorphism
by YELLOW12:43;
then
Y is
closed
by A25, A27, TOPS_2:58;
hence
A is
closed
by A23, A24, A25;
verum
end;
hence
N is Hausdorff
by YELLOW12:46; verum