let L be complete LATTICE; ( ( for x being Element of L holds x is compact ) iff for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) ) )
hereby ( ( for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) ) ) implies for x being Element of L holds x is compact )
assume A1:
for
x being
Element of
L holds
x is
compact
;
for Y being non empty Subset of L ex x being Element of L st
( x in Y & ( for y being Element of L holds
( not y in Y or not x < y ) ) )given Y being non
empty Subset of
L such that A2:
for
x being
Element of
L st
x in Y holds
ex
y being
Element of
L st
(
y in Y &
x < y )
;
contradictiondefpred S1[
set ,
set ]
means (
[$1,$2] in the
InternalRel of
L & $1
<> $2 );
consider f being
Function such that A7:
(
dom f = Y &
rng f c= Y & ( for
x being
set st
x in Y holds
S1[
x,
f . x] ) )
from WELLORD2:sch 1(A3);
consider x being
Element of
Y;
set x1 =
x;
set Z =
{ ((iter f,n) . x) where n is Element of NAT : verum } ;
f . x in rng f
by A7, FUNCT_1:def 5;
then
f . x in Y
by A7;
then reconsider x =
x,
x9 =
f . x as
Element of
L ;
A8:
[x,(f . x)] in the
InternalRel of
L
by A7;
A9:
x <> f . x
by A7;
A10:
x9 = (iter f,1) . x
by FUNCT_7:72;
A11:
x <= x9
by A8, ORDERS_2:def 9;
A12:
x9 in { ((iter f,n) . x) where n is Element of NAT : verum }
by A10;
A13:
x < x9
by A9, A11, ORDERS_2:def 10;
A14:
{ ((iter f,n) . x) where n is Element of NAT : verum } c= Y
then reconsider Z =
{ ((iter f,n) . x) where n is Element of NAT : verum } as
Subset of
L by XBOOLE_1:1;
A17:
now let i be
Element of
NAT ;
for k being Element of NAT st i <= k holds
for z, y being Element of L st z = (iter f,i) . x & y = (iter f,k) . x holds
z <= ydefpred S2[
Element of
NAT ]
means ex
z,
y being
Element of
L st
(
z = (iter f,i) . x &
y = (iter f,(i + $1)) . x &
z <= y );
(iter f,i) . x in Z
;
then A18:
S2[
0 ]
;
A19:
for
k being
Element of
NAT st
S2[
k] holds
S2[
k + 1]
proof
let k be
Element of
NAT ;
( S2[k] implies S2[k + 1] )
given z,
y being
Element of
L such that A20:
z = (iter f,i) . x
and A21:
y = (iter f,(i + k)) . x
and A22:
z <= y
;
S2[k + 1]
take
z
;
ex y being Element of L st
( z = (iter f,i) . x & y = (iter f,(i + (k + 1))) . x & z <= y )
A23:
rng (iter f,(i + k)) c= Y
by A7, FUNCT_7:76;
A24:
dom (iter f,(i + k)) = Y
by A7, FUNCT_7:76;
then A25:
y in rng (iter f,(i + k))
by A21, FUNCT_1:def 5;
then
f . y in rng f
by A7, A23, FUNCT_1:def 5;
then
f . y in Y
by A7;
then reconsider yy =
f . y as
Element of
L ;
take
yy
;
( z = (iter f,i) . x & yy = (iter f,(i + (k + 1))) . x & z <= yy )
thus
z = (iter f,i) . x
by A20;
( yy = (iter f,(i + (k + 1))) . x & z <= yy )
iter f,
((k + i) + 1) = f * (iter f,(k + i))
by FUNCT_7:73;
hence
yy = (iter f,(i + (k + 1))) . x
by A21, A24, FUNCT_1:23;
z <= yy
[y,yy] in the
InternalRel of
L
by A7, A23, A25;
then
y <= yy
by ORDERS_2:def 9;
hence
z <= yy
by A22, ORDERS_2:26;
verum
end; A26:
for
k being
Element of
NAT holds
S2[
k]
from NAT_1:sch 1(A18, A19);
let k be
Element of
NAT ;
( i <= k implies for z, y being Element of L st z = (iter f,i) . x & y = (iter f,k) . x holds
z <= y )assume
i <= k
;
for z, y being Element of L st z = (iter f,i) . x & y = (iter f,k) . x holds
z <= ythen consider n being
Nat such that A27:
k = i + n
by NAT_1:10;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
A28:
ex
z,
y being
Element of
L st
(
z = (iter f,i) . x &
y = (iter f,(i + n)) . x &
z <= y )
by A26;
let z,
y be
Element of
L;
( z = (iter f,i) . x & y = (iter f,k) . x implies z <= y )assume that A29:
z = (iter f,i) . x
and A30:
y = (iter f,k) . x
;
z <= ythus
z <= y
by A27, A28, A29, A30;
verum end;
sup Z is
compact
by A1;
then
sup Z << sup Z
by Def2;
then consider A being
finite Subset of
L such that A34:
A c= Z
and A35:
sup Z <= sup A
by Th18;
A40:
A is
finite
;
defpred S2[
set ]
means ( $1
<> {} implies
"\/" $1,
L in $1 );
A41:
S2[
{} ]
;
A42:
now let x,
B be
set ;
( x in A & B c= A & S2[B] implies S2[B \/ {x}] )assume that A43:
x in A
and A44:
B c= A
;
( S2[B] implies S2[B \/ {x}] )reconsider x9 =
x as
Element of
L by A43;
assume A45:
S2[
B]
;
S2[B \/ {x}]thus
S2[
B \/ {x}]
verumproof
assume
B \/ {x} <> {}
;
"\/" (B \/ {x}),L in B \/ {x}
A46:
ex_sup_of B,
L
by YELLOW_0:17;
A47:
ex_sup_of {x},
L
by YELLOW_0:17;
ex_sup_of B \/ {x},
L
by YELLOW_0:17;
then A48:
"\/" (B \/ {x}),
L = ("\/" B,L) "\/" ("\/" {x},L)
by A46, A47, YELLOW_0:36;
A49:
sup {x9} = x
by YELLOW_0:39;
per cases
( B = {} or B <> {} )
;
suppose
B <> {}
;
"\/" (B \/ {x}),L in B \/ {x}then
"\/" B,
L in A
by A44, A45;
then
(
x9 <= "\/" B,
L or
x9 >= "\/" B,
L )
by A31, A34, A43;
then
(
("\/" B,L) "\/" x9 = "\/" B,
L or (
("\/" B,L) "\/" x9 = x9 "\/" ("\/" B,L) &
x9 "\/" ("\/" B,L) = x9 ) )
by YELLOW_0:24;
then
(
"\/" (B \/ {x}),
L in B or
"\/" (B \/ {x}),
L in {x} )
by A45, A48, A49, TARSKI:def 1;
hence
"\/" (B \/ {x}),
L in B \/ {x}
by XBOOLE_0:def 3;
verum end;
end; end;
S2[
A]
from FINSET_1:sch 2(A40, A41, A42);
then A50:
sup A in Z
by A34, A36;
then consider n being
Element of
NAT such that A51:
sup A = (iter f,n) . x
;
A52:
[(sup A),(f . (sup A))] in the
InternalRel of
L
by A7, A14, A50;
A53:
sup A <> f . (sup A)
by A7, A14, A50;
reconsider xSn =
f . (sup A) as
Element of
L by A52, ZFMISC_1:106;
A54:
iter f,
(n + 1) = f * (iter f,n)
by FUNCT_7:73;
A55:
dom (iter f,n) = Y
by A7, FUNCT_7:76;
A56:
sup A <= xSn
by A52, ORDERS_2:def 9;
A57:
f . (sup A) = (iter f,(n + 1)) . x
by A51, A54, A55, FUNCT_1:23;
A58:
sup A < xSn
by A53, A56, ORDERS_2:def 10;
A59:
xSn in Z
by A57;
Z is_<=_than sup Z
by YELLOW_0:32;
then A60:
xSn <= sup Z
by A59, LATTICE3:def 9;
sup Z < xSn
by A35, A58, ORDERS_2:32;
hence
contradiction
by A60, ORDERS_2:30;
verum
end;
assume A61:
for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) )
; for x being Element of L holds x is compact
let x be Element of L; x is compact
let D be non empty directed Subset of L; WAYBEL_3:def 1,WAYBEL_3:def 2 ( x <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
consider y being Element of L such that
A62:
y in D
and
A63:
for z being Element of L st z in D holds
not y < z
by A61;
D is_<=_than y
then A67:
sup D <= y
by YELLOW_0:32;
sup D is_>=_than D
by YELLOW_0:32;
then
y <= sup D
by A62, LATTICE3:def 9;
then
sup D = y
by A67, ORDERS_2:25;
hence
( x <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
by A62; verum