let L be complete LATTICE; :: thesis: ( ( 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 :: thesis: ( ( 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
;
:: thesis: 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 )
;
:: thesis: contradictiondefpred S1[
set ,
set ]
means (
[$1,$2] in the
InternalRel of
L & $1
<> $2 );
consider f being
Function such that A6:
(
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 A6, FUNCT_1:def 5;
then
f . x in Y
by A6;
then reconsider x =
x,
x' =
f . x as
Element of
L ;
A7:
(
[x,(f . x)] in the
InternalRel of
L &
x <> f . x )
by A6;
then
(
x' = (iter f,1) . x &
x <= x' )
by FUNCT_7:72, ORDERS_2:def 9;
then A8:
(
x' in { ((iter f,n) . x) where n is Element of NAT : verum } &
x < x' )
by A7, ORDERS_2:def 10;
A9:
{ ((iter f,n) . x) where n is Element of NAT : verum } c= Y
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in { ((iter f,n) . x) where n is Element of NAT : verum } or a in Y )
assume
a in { ((iter f,n) . x) where n is Element of NAT : verum }
;
:: thesis: a in Y
then consider n being
Element of
NAT such that A10:
a = (iter f,n) . x
;
dom (iter f,n) = Y
by A6, FUNCT_7:76;
then
(
a in rng (iter f,n) &
rng (iter f,n) c= Y )
by A6, A10, FUNCT_1:def 5, FUNCT_7:76;
hence
a in Y
;
:: thesis: verum
end; then reconsider Z =
{ ((iter f,n) . x) where n is Element of NAT : verum } as
Subset of
L by XBOOLE_1:1;
A11:
now let i be
Element of
NAT ;
:: thesis: 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 A12:
S2[
0 ]
;
A13:
for
k being
Element of
NAT st
S2[
k] holds
S2[
k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S2[k] implies S2[k + 1] )
given z,
y being
Element of
L such that A14:
(
z = (iter f,i) . x &
y = (iter f,(i + k)) . x &
z <= y )
;
:: thesis: S2[k + 1]
take
z
;
:: thesis: ex y being Element of L st
( z = (iter f,i) . x & y = (iter f,(i + (k + 1))) . x & z <= y )
A15:
(
rng (iter f,(i + k)) c= Y &
dom (iter f,(i + k)) = Y )
by A6, FUNCT_7:76;
then A16:
y in rng (iter f,(i + k))
by A14, FUNCT_1:def 5;
then
f . y in rng f
by A6, A15, FUNCT_1:def 5;
then
f . y in Y
by A6;
then reconsider yy =
f . y as
Element of
L ;
take
yy
;
:: thesis: ( z = (iter f,i) . x & yy = (iter f,(i + (k + 1))) . x & z <= yy )
thus
z = (iter f,i) . x
by A14;
:: thesis: ( yy = (iter f,(i + (k + 1))) . x & z <= yy )
(
i + (k + 1) = (i + k) + 1 &
iter f,
((k + i) + 1) = f * (iter f,(k + i)) )
by FUNCT_7:73;
hence
yy = (iter f,(i + (k + 1))) . x
by A14, A15, FUNCT_1:23;
:: thesis: z <= yy
[y,yy] in the
InternalRel of
L
by A6, A15, A16;
then
y <= yy
by ORDERS_2:def 9;
hence
z <= yy
by A14, ORDERS_2:26;
:: thesis: verum
end; A17:
for
k being
Element of
NAT holds
S2[
k]
from NAT_1:sch 1(A12, A13);
let k be
Element of
NAT ;
:: thesis: ( 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
;
:: thesis: 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 A18:
k = i + n
by NAT_1:10;
reconsider n =
n as
Element of
NAT by ORDINAL1:def 13;
A19:
ex
z,
y being
Element of
L st
(
z = (iter f,i) . x &
y = (iter f,(i + n)) . x &
z <= y )
by A17;
let z,
y be
Element of
L;
:: thesis: ( z = (iter f,i) . x & y = (iter f,k) . x implies z <= y )assume
(
z = (iter f,i) . x &
y = (iter f,k) . x )
;
:: thesis: z <= yhence
z <= y
by A18, A19;
:: thesis: verum end;
sup Z is
compact
by A1;
then
(
sup Z <= sup Z &
sup Z << sup Z )
by Def2;
then consider A being
finite Subset of
L such that A23:
(
A c= Z &
sup Z <= sup A )
by Th18;
A25:
A is
finite
;
defpred S2[
set ]
means ( $1
<> {} implies
"\/" $1,
L in $1 );
A26:
S2[
{} ]
;
A27:
now let x,
B be
set ;
:: thesis: ( x in A & B c= A & S2[B] implies S2[B \/ {x}] )assume A28:
(
x in A &
B c= A )
;
:: thesis: ( S2[B] implies S2[B \/ {x}] )then reconsider x' =
x as
Element of
L ;
assume A29:
S2[
B]
;
:: thesis: S2[B \/ {x}]thus
S2[
B \/ {x}]
:: thesis: verumproof
assume
B \/ {x} <> {}
;
:: thesis: "\/" (B \/ {x}),L in B \/ {x}
(
ex_sup_of B,
L &
ex_sup_of {x},
L &
ex_sup_of B \/ {x},
L )
by YELLOW_0:17;
then A30:
(
"\/" (B \/ {x}),
L = ("\/" B,L) "\/" ("\/" {x},L) &
sup {x'} = x )
by YELLOW_0:36, YELLOW_0:39;
per cases
( B = {} or B <> {} )
;
suppose
B <> {}
;
:: thesis: "\/" (B \/ {x}),L in B \/ {x}then
"\/" B,
L in A
by A28, A29;
then
(
x' <= "\/" B,
L or
x' >= "\/" B,
L )
by A20, A23, A28;
then
(
("\/" B,L) "\/" x' = "\/" B,
L or (
("\/" B,L) "\/" x' = x' "\/" ("\/" B,L) &
x' "\/" ("\/" B,L) = x' ) )
by YELLOW_0:24;
then
(
"\/" (B \/ {x}),
L in B or
"\/" (B \/ {x}),
L in {x} )
by A29, A30, TARSKI:def 1;
hence
"\/" (B \/ {x}),
L in B \/ {x}
by XBOOLE_0:def 3;
:: thesis: verum end;
end; end;
S2[
A]
from FINSET_1:sch 2(A25, A26, A27);
then A31:
sup A in Z
by A23, A24;
then consider n being
Element of
NAT such that A32:
sup A = (iter f,n) . x
;
A33:
(
[(sup A),(f . (sup A))] in the
InternalRel of
L &
sup A <> f . (sup A) )
by A6, A9, A31;
then reconsider xSn =
f . (sup A) as
Element of
L by ZFMISC_1:106;
(
iter f,
(n + 1) = f * (iter f,n) &
dom (iter f,n) = Y )
by A6, FUNCT_7:73, FUNCT_7:76;
then
(
sup A <= xSn &
f . (sup A) = (iter f,(n + 1)) . x )
by A32, A33, FUNCT_1:23, ORDERS_2:def 9;
then
(
sup A < xSn &
xSn in Z &
Z is_<=_than sup Z )
by A33, ORDERS_2:def 10, YELLOW_0:32;
then
(
xSn <= sup Z &
sup Z < xSn )
by A23, LATTICE3:def 9, ORDERS_2:32;
hence
contradiction
by ORDERS_2:30;
:: thesis: verum
end;
assume A34:
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 ) )
; :: thesis: for x being Element of L holds x is compact
let x be Element of L; :: thesis: x is compact
let D be non empty directed Subset of L; :: according to WAYBEL_3:def 1,WAYBEL_3:def 2 :: thesis: ( x <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
consider y being Element of L such that
A35:
( y in D & ( for z being Element of L st z in D holds
not y < z ) )
by A34;
D is_<=_than y
then A37:
sup D <= y
by YELLOW_0:32;
sup D is_>=_than D
by YELLOW_0:32;
then
y <= sup D
by A35, LATTICE3:def 9;
then
sup D = y
by A37, ORDERS_2:25;
hence
( x <= sup D implies ex d being Element of L st
( d in D & x <= d ) )
by A35; :: thesis: verum