let L be finite Lattice; :: thesis: L is complete
for X being Subset of L ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) )
proof
let X be
Subset of
L;
:: thesis: ex a being Element of L st
( a is_less_than X & ( for b being Element of L st b is_less_than X holds
b [= a ) )
defpred S1[
Element of
NAT ]
means for
X' being
finite Subset of
(LattPOSet L) for
p being
FinSequence st
rng p = X' &
len p = $1 holds
ex
a being
Element of
(LattPOSet L) st
( ( for
x being
Element of
(LattPOSet L) st
x in X' holds
a <= x ) & ( for
x' being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in X' holds
x' <= x ) holds
x' <= a ) );
A1:
S1[
0 ]
A6:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A7:
S1[
k]
;
:: thesis: S1[k + 1]
for
X' being
finite Subset of
(LattPOSet L) for
p being
FinSequence st
rng p = X' &
len p = k + 1 holds
ex
a being
Element of
(LattPOSet L) st
( ( for
x being
Element of
(LattPOSet L) st
x in X' holds
a <= x ) & ( for
x' being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in X' holds
x' <= x ) holds
x' <= a ) )
proof
let X be
finite Subset of
(LattPOSet L);
:: thesis: for p being FinSequence st rng p = X & len p = k + 1 holds
ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X holds
a <= x ) & ( for x' being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X holds
x' <= x ) holds
x' <= a ) )let p be
FinSequence;
:: thesis: ( rng p = X & len p = k + 1 implies ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X holds
a <= x ) & ( for x' being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X holds
x' <= x ) holds
x' <= a ) ) )
assume A8:
(
rng p = X &
len p = k + 1 )
;
:: thesis: ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X holds
a <= x ) & ( for x' being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X holds
x' <= x ) holds
x' <= a ) )
set q =
p | (Seg k);
set X' =
rng (p | (Seg k));
A9:
k <= k + 1
by NAT_1:11;
then A10:
len (p | (Seg k)) = k
by A8, FINSEQ_1:21;
for
x being
set st
x in rng (p | (Seg k)) holds
x in the
carrier of
(LattPOSet L)
then
rng (p | (Seg k)) is
Subset of
(LattPOSet L)
by TARSKI:def 3;
then consider a being
Element of
(LattPOSet L) such that A12:
( ( for
x being
Element of
(LattPOSet L) st
x in rng (p | (Seg k)) holds
a <= x ) & ( for
x' being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in rng (p | (Seg k)) holds
x' <= x ) holds
x' <= a ) )
by A7, A10;
consider b being
set such that A13:
p . (k + 1) = b
;
Seg (k + 1) = dom p
by A8, FINSEQ_1:def 3;
then
k + 1
in dom p
by FINSEQ_1:6;
then A14:
b in rng p
by A13, FUNCT_1:def 5;
then reconsider b =
b as
Element of
(LattPOSet L) by A8;
set a2 =
(% a) "/\" (% b);
A15:
((% a) "/\" (% b)) "\/" (% a) = % a
by LATTICES:def 8;
((% a) "/\" (% b)) "\/" (% b) = % b
by LATTICES:def 8;
then A16:
(
(% a) "/\" (% b) [= % a &
(% a) "/\" (% b) [= % b )
by A15, LATTICES:def 3;
A17:
(% a) % =
% a
by LATTICE3:def 3
.=
a
by LATTICE3:def 4
;
A18:
(% b) % =
% b
by LATTICE3:def 3
.=
b
by LATTICE3:def 4
;
A19:
for
x being
Element of
(LattPOSet L) st
x in X holds
((% a) "/\" (% b)) % <= x
proof
let c be
Element of
(LattPOSet L);
:: thesis: ( c in X implies ((% a) "/\" (% b)) % <= c )
assume A20:
c in X
;
:: thesis: ((% a) "/\" (% b)) % <= c
per cases
( c in rng (p | (Seg k)) or not c in rng (p | (Seg k)) )
;
suppose A21:
not
c in rng (p | (Seg k))
;
:: thesis: ((% a) "/\" (% b)) % <= cconsider n being
set such that A22:
(
n in dom p &
c = p . n )
by A8, A20, FUNCT_1:def 5;
reconsider n =
n as
Element of
NAT by A22;
A23:
n in Seg (k + 1)
by A8, A22, FINSEQ_1:def 3;
then A24:
( 1
<= n &
n <= k + 1 )
by FINSEQ_1:3;
n >= k + 1
proof
assume
not
n >= k + 1
;
:: thesis: contradiction
then
( 1
<= n &
n <= k )
by A23, FINSEQ_1:3, INT_1:20;
then A25:
n in Seg k
by FINSEQ_1:3;
then A26:
n in dom (p | (Seg k))
by A8, A9, FINSEQ_1:21;
dom (p | (Seg k)) =
(dom p) /\ (Seg k)
by RELAT_1:90
.=
(Seg (k + 1)) /\ (Seg k)
by A8, FINSEQ_1:def 3
.=
Seg k
by FINSEQ_1:9, NAT_1:11
;
then
(p | (Seg k)) . n = c
by A22, A25, FUNCT_1:70;
hence
contradiction
by A21, A26, FUNCT_1:def 5;
:: thesis: verum
end; then
c = b
by A13, A22, A24, XXREAL_0:1;
hence
((% a) "/\" (% b)) % <= c
by A16, A18, LATTICE3:7;
:: thesis: verum end;
end;
for
x' being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in X holds
x' <= x ) holds
x' <= ((% a) "/\" (% b)) %
hence
ex
a being
Element of
(LattPOSet L) st
( ( for
x being
Element of
(LattPOSet L) st
x in X holds
a <= x ) & ( for
x' being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in X holds
x' <= x ) holds
x' <= a ) )
by A19;
:: thesis: verum
end;
hence
S1[
k + 1]
;
:: thesis: verum
end;
A34:
for
k being
Element of
NAT holds
S1[
k]
from NAT_1:sch 1(A1, A6);
reconsider X =
X as
finite Subset of
L ;
LattPOSet L = RelStr(# the
carrier of
L,
(LattRel L) #)
by LATTICE3:def 2;
then reconsider X' =
X as
finite Subset of
(LattPOSet L) ;
consider p being
FinSequence such that A35:
rng p = X'
by FINSEQ_1:73;
dom p = Seg (len p)
by FINSEQ_1:def 3;
then consider a being
Element of
(LattPOSet L) such that A36:
( ( for
x being
Element of
(LattPOSet L) st
x in X' holds
a <= x ) & ( for
x' being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in X' holds
x' <= x ) holds
x' <= a ) )
by A34, A35;
for
x being
Element of
L st
x in X holds
% a [= x
then A40:
% a is_less_than X
by LATTICE3:def 16;
for
b being
Element of
L st
b is_less_than X holds
b [= % a
hence
ex
a being
Element of
L st
(
a is_less_than X & ( for
b being
Element of
L st
b is_less_than X holds
b [= a ) )
by A40;
:: thesis: verum
end;
hence
L is complete
by VECTSP_8:def 6; :: thesis: verum