let L be finite Lattice; 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
defpred S1[
Nat]
means for
X9 being
finite Subset of
(LattPOSet L) for
p being
FinSequence st
rng p = X9 &
len p = $1 holds
ex
a being
Element of
(LattPOSet L) st
( ( for
x being
Element of
(LattPOSet L) st
x in X9 holds
a <= x ) & ( for
x9 being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in X9 holds
x9 <= x ) holds
x9 <= a ) );
let X be
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 ) )
A1:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A2:
S1[
k]
;
S1[k + 1]
for
X9 being
finite Subset of
(LattPOSet L) for
p being
FinSequence st
rng p = X9 &
len p = k + 1 holds
ex
a being
Element of
(LattPOSet L) st
( ( for
x being
Element of
(LattPOSet L) st
x in X9 holds
a <= x ) & ( for
x9 being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in X9 holds
x9 <= x ) holds
x9 <= a ) )
proof
let X be
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 x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X holds
x9 <= x ) holds
x9 <= a ) )let p be
FinSequence;
( 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 x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X holds
x9 <= x ) holds
x9 <= a ) ) )
assume that A3:
rng p = X
and A4:
len p = k + 1
;
ex a being Element of (LattPOSet L) st
( ( for x being Element of (LattPOSet L) st x in X holds
a <= x ) & ( for x9 being Element of (LattPOSet L) st ( for x being Element of (LattPOSet L) st x in X holds
x9 <= x ) holds
x9 <= a ) )
set q =
p | (Seg k);
set X9 =
rng (p | (Seg k));
for
x being
object st
x in rng (p | (Seg k)) holds
x in the
carrier of
(LattPOSet L)
then A6:
rng (p | (Seg k)) is
Subset of
(LattPOSet L)
by TARSKI:def 3;
A7:
k <= k + 1
by NAT_1:11;
then
len (p | (Seg k)) = k
by A4, FINSEQ_1:17;
then consider a being
Element of
(LattPOSet L) such that A8:
for
x being
Element of
(LattPOSet L) st
x in rng (p | (Seg k)) holds
a <= x
and A9:
for
x9 being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in rng (p | (Seg k)) holds
x9 <= x ) holds
x9 <= a
by A2, A6;
consider b being
set such that A10:
p . (k + 1) = b
;
Seg (k + 1) = dom p
by A4, FINSEQ_1:def 3;
then
k + 1
in dom p
by FINSEQ_1:4;
then A11:
b in rng p
by A10, FUNCT_1:def 3;
then reconsider b =
b as
Element of
(LattPOSet L) by A3;
A12:
(% b) % =
% b
by LATTICE3:def 3
.=
b
by LATTICE3:def 4
;
set a2 =
(% a) "/\" (% b);
((% a) "/\" (% b)) "\/" (% a) = % a
by LATTICES:def 8;
then A13:
(% a) "/\" (% b) [= % a
by LATTICES:def 3;
((% a) "/\" (% b)) "\/" (% b) = % b
by LATTICES:def 8;
then A14:
(% a) "/\" (% b) [= % b
by LATTICES:def 3;
A15:
(% a) % =
% a
by LATTICE3:def 3
.=
a
by LATTICE3:def 4
;
A16:
for
x being
Element of
(LattPOSet L) st
x in X holds
((% a) "/\" (% b)) % <= x
proof
let c be
Element of
(LattPOSet L);
( c in X implies ((% a) "/\" (% b)) % <= c )
assume A17:
c in X
;
((% a) "/\" (% b)) % <= c
per cases
( c in rng (p | (Seg k)) or not c in rng (p | (Seg k)) )
;
suppose A19:
not
c in rng (p | (Seg k))
;
((% a) "/\" (% b)) % <= cconsider n being
object such that A20:
n in dom p
and A21:
c = p . n
by A3, A17, FUNCT_1:def 3;
reconsider n =
n as
Element of
NAT by A20;
A22:
n in Seg (k + 1)
by A4, A20, FINSEQ_1:def 3;
A23:
n >= k + 1
proof
assume
not
n >= k + 1
;
contradiction
then A24:
n <= k
by INT_1:7;
1
<= n
by A22, FINSEQ_1:1;
then A25:
n in Seg k
by A24, FINSEQ_1:1;
dom (p | (Seg k)) =
(dom p) /\ (Seg k)
by RELAT_1:61
.=
(Seg (k + 1)) /\ (Seg k)
by A4, FINSEQ_1:def 3
.=
Seg k
by FINSEQ_1:7, NAT_1:11
;
then A26:
(p | (Seg k)) . n = c
by A21, A25, FUNCT_1:47;
n in dom (p | (Seg k))
by A4, A7, A25, FINSEQ_1:17;
hence
contradiction
by A19, A26, FUNCT_1:def 3;
verum
end;
n <= k + 1
by A22, FINSEQ_1:1;
then
c = b
by A10, A21, A23, XXREAL_0:1;
hence
((% a) "/\" (% b)) % <= c
by A14, A12, LATTICE3:7;
verum end;
end;
for
x9 being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in X holds
x9 <= x ) holds
x9 <= ((% 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
x9 being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in X holds
x9 <= x ) holds
x9 <= a ) )
by A16;
verum
end;
hence
S1[
k + 1]
;
verum
end;
for
X9 being
finite Subset of
(LattPOSet L) for
p being
FinSequence st
rng p = X9 &
len p = 0 holds
ex
a being
Element of
(LattPOSet L) st
( ( for
x being
Element of
(LattPOSet L) st
x in X9 holds
a <= x ) & ( for
x9 being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in X9 holds
x9 <= x ) holds
x9 <= a ) )
then A38:
S1[
0 ]
;
A39:
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A38, A1);
reconsider X =
X as
finite Subset of
L ;
LattPOSet L = RelStr(# the
carrier of
L,
(LattRel L) #)
by LATTICE3:def 2;
then reconsider X9 =
X as
finite Subset of
(LattPOSet L) ;
consider p being
FinSequence such that A40:
rng p = X9
by FINSEQ_1:52;
dom p = Seg (len p)
by FINSEQ_1:def 3;
then consider a being
Element of
(LattPOSet L) such that A41:
for
x being
Element of
(LattPOSet L) st
x in X9 holds
a <= x
and A42:
for
x9 being
Element of
(LattPOSet L) st ( for
x being
Element of
(LattPOSet L) st
x in X9 holds
x9 <= x ) holds
x9 <= a
by A39, A40;
A43:
for
b being
Element of
L st
b is_less_than X holds
b [= % a
for
x being
Element of
L st
x in X holds
% a [= x
then
% a is_less_than X
by LATTICE3:def 16;
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 A43;
verum
end;
hence
L is complete
by VECTSP_8:def 6; verum