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[
object ,
object ]
means (
[$1,$2] in the
InternalRel of
L & $1
<> $2 );
A3:
now for x being object st x in Y holds
ex u being object st
( u in Y & S1[x,u] )let x be
object ;
( x in Y implies ex u being object st
( u in Y & S1[x,u] ) )assume A4:
x in Y
;
ex u being object st
( u in Y & S1[x,u] )then reconsider y =
x as
Element of
L ;
consider z being
Element of
L such that A5:
z in Y
and A6:
y < z
by A2, A4;
reconsider u =
z as
object ;
take u =
u;
( u in Y & S1[x,u] )
y <= z
by A6;
hence
(
u in Y &
S1[
x,
u] )
by A5, A6;
verum end; consider f being
Function such that A7:
(
dom f = Y &
rng f c= Y & ( for
x being
object st
x in Y holds
S1[
x,
f . x] ) )
from FUNCT_1:sch 6(A3);
set x = the
Element of
Y;
set x1 = the
Element of
Y;
set Z =
{ ((iter (f,n)) . the Element of Y) where n is Element of NAT : verum } ;
f . the
Element of
Y in rng f
by A7, FUNCT_1:def 3;
then
f . the
Element of
Y in Y
by A7;
then reconsider x = the
Element of
Y,
x9 =
f . the
Element of
Y 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:70;
A11:
x <= x9
by A8;
A12:
x9 in { ((iter (f,n)) . the Element of Y) where n is Element of NAT : verum }
by A10;
A13:
x < x9
by A9, A11;
A14:
{ ((iter (f,n)) . the Element of Y) where n is Element of NAT : verum } c= Y
then reconsider Z =
{ ((iter (f,n)) . the Element of Y) where n is Element of NAT : verum } as
Subset of
L by XBOOLE_1:1;
A17:
now for i, 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 <= ylet 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[
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
Nat st
S2[
k] holds
S2[
k + 1]
proof
let k be
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:74;
A24:
dom (iter (f,(i + k))) = Y
by A7, FUNCT_7:74;
then A25:
y in rng (iter (f,(i + k)))
by A21, FUNCT_1:def 3;
then
f . y in rng f
by A7, A23, FUNCT_1:def 3;
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:71;
hence
yy = (iter (f,(i + (k + 1)))) . x
by A21, A24, FUNCT_1:13;
z <= yy
[y,yy] in the
InternalRel of
L
by A7, A23, A25;
then
y <= yy
;
hence
z <= yy
by A22, ORDERS_2:3;
verum
end; A26:
for
k being
Nat holds
S2[
k]
from NAT_1:sch 2(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 12;
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; A31:
now for z, y being Element of L holds
( not z in Z or not y in Z or z <= y or z >= y )end;
sup Z is
compact
by A1;
then
sup Z << sup Z
;
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 for x, B being set st x in A & B c= A & S2[B] holds
S2[B \/ {x}]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:87;
A54:
iter (
f,
(n + 1))
= f * (iter (f,n))
by FUNCT_7:71;
A55:
dom (iter (f,n)) = Y
by A7, FUNCT_7:74;
A56:
sup A <= xSn
by A52;
A57:
f . (sup A) = (iter (f,(n + 1))) . x
by A51, A54, A55, FUNCT_1:13;
A58:
sup A < xSn
by A53, A56;
A59:
xSn in Z
by A57;
Z is_<=_than sup Z
by YELLOW_0:32;
then A60:
xSn <= sup Z
by A59;
sup Z < xSn
by A35, A58, ORDERS_2:7;
hence
contradiction
by A60, ORDERS_2:6;
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;
then
sup D = y
by A67, ORDERS_2:2;
hence
( x <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
by A62; verum