let N be complete Lawson TopLattice; :: thesis: ( N is continuous iff ( N is meet-continuous & N is T_2 ) )
thus
( N is continuous implies ( N is meet-continuous & N is T_2 ) )
; :: thesis: ( N is meet-continuous & N is T_2 implies N is continuous )
assume A1:
( N is meet-continuous & N is T_2 )
; :: thesis: N is continuous
thus A2:
for x being Element of N holds
( not waybelow x is empty & waybelow x is directed )
; :: according to WAYBEL_3:def 6 :: thesis: ( N is up-complete & N is satisfying_axiom_of_approximation )
thus
N is up-complete
; :: thesis: N is satisfying_axiom_of_approximation
for x, y being Element of N st not x <= y holds
ex u being Element of N st
( u << x & not u <= y )
proof
let x,
y be
Element of
N;
:: thesis: ( not x <= y implies ex u being Element of N st
( u << x & not u <= y ) )
assume A3:
not
x <= y
;
:: thesis: ex u being Element of N st
( u << x & not u <= y )
consider S being
Scott TopAugmentation of
N;
A4:
RelStr(# the
carrier of
S,the
InternalRel of
S #)
= RelStr(# the
carrier of
N,the
InternalRel of
N #)
by YELLOW_9:def 4;
reconsider J =
{ (O \ (uparrow F)) where O, F is Subset of N : ( O in sigma N & F is finite ) } as
Basis of
N by WAYBEL19:32;
x "/\" y <> x
by A3, YELLOW_0:23;
then consider W,
V being
Subset of
N such that A5:
W is
open
and A6:
V is
open
and A7:
(
x in W &
x "/\" y in V &
W misses V )
by A1, PRE_TOPC:def 16;
V = union { G where G is Subset of N : ( G in J & G c= V ) }
by A6, YELLOW_8:18;
then consider K being
set such that A8:
(
x "/\" y in K &
K in { G where G is Subset of N : ( G in J & G c= V ) } )
by A7, TARSKI:def 4;
consider V1 being
Subset of
N such that A9:
(
K = V1 &
V1 in J &
V1 c= V )
by A8;
consider U2,
F being
Subset of
N such that A10:
V1 = U2 \ (uparrow F)
and A11:
U2 in sigma N
and A12:
F is
finite
by A9;
reconsider U1 =
U2 as
Subset of
S by A4;
U2 in sigma S
by A4, A11, YELLOW_9:52;
then A13:
U1 is
open
by WAYBEL14:24;
reconsider WU1 =
W /\ U2 as
Subset of
N ;
WU1 c= uparrow F
then
WU1 is_coarser_than uparrow F
by WAYBEL12:20;
then A18:
uparrow WU1 c= uparrow F
by YELLOW12:28;
reconsider W1 =
WU1 as
Subset of
S by A4;
reconsider F1 =
F as
finite Subset of
S by A4, A12;
S is
meet-continuous
by A1, A4, YELLOW12:14;
then A19:
Int (uparrow F1) c= union { (wayabove u) where u is Element of S : u in F1 }
by Th29;
A20:
(
uparrow W1 = uparrow WU1 &
uparrow F1 = uparrow F )
by A4, WAYBEL_0:13;
reconsider x1 =
x,
y1 =
y as
Element of
S by A4;
A21:
ex_inf_of {x1,y1},
S
by YELLOW_0:21;
x "/\" y =
inf {x,y}
by YELLOW_0:40
.=
"/\" {x1,y1},
S
by A4, A21, YELLOW_0:27
.=
x1 "/\" y1
by YELLOW_0:40
;
then A22:
x1 "/\" y1 in U1
by A8, A9, A10, XBOOLE_0:def 5;
A23:
x1 "/\" y1 <= x1
by YELLOW_0:23;
U1 is
upper
by A13, WAYBEL11:def 4;
then
x1 in U1
by A22, A23, WAYBEL_0:def 20;
then A24:
x in W1
by A7, XBOOLE_0:def 4;
W1 c= uparrow W1
by WAYBEL_0:16;
then A25:
x in uparrow W1
by A24;
N is
correct Lawson TopAugmentation of
S
by A4, YELLOW_9:def 4;
then
U2 is
open
by A13, WAYBEL19:37;
then
WU1 is
open
by A5, TOPS_1:38;
then
uparrow W1 c= Int (uparrow F1)
by A1, A18, A20, Th15, TOPS_1:56;
then
x in Int (uparrow F1)
by A25;
then consider A being
set such that A26:
(
x in A &
A in { (wayabove u) where u is Element of S : u in F1 } )
by A19, TARSKI:def 4;
consider u being
Element of
S such that A27:
(
A = wayabove u &
u in F1 )
by A26;
reconsider u1 =
u as
Element of
N by A4;
A28:
wayabove u1 = wayabove u
by A4, YELLOW12:13;
A29:
for
N being
Semilattice for
x,
y being
Element of
N st ex
u being
Element of
N st
(
u << x & not
u <= x "/\" y ) holds
ex
u being
Element of
N st
(
u << x & not
u <= y )
then consider u2 being
Element of
N such that A33:
(
u2 << x & not
u2 <= y )
by A29;
take
u2
;
:: thesis: ( u2 << x & not u2 <= y )
thus
(
u2 << x & not
u2 <= y )
by A33;
:: thesis: verum
end;
hence
N is satisfying_axiom_of_approximation
by A2, WAYBEL_3:24; :: thesis: verum