defpred S1[ Nat] means for L being finite Lattice
for X being Subset of (LattPOSet L)
for p being FinSequence st rng p = X & len p = $1 & not X is empty holds
ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a;
let L be finite Lattice; for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
let X be Subset of L; ( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in 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]
per cases
( k = 0 or k <> 0 )
;
suppose A8:
k <> 0
;
S1[k + 1]
for
L being
finite Lattice for
X being
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
b being
Element of
(LattPOSet L) st
b in X holds
b <= a
proof
let L be
finite Lattice;
for X being 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 b being Element of (LattPOSet L) st b in X holds
b <= alet X be
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 b being Element of (LattPOSet L) st b in X holds
b <= alet p be
FinSequence;
( rng p = X & len p = k + 1 implies ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
assume that A9:
rng p = X
and A10:
len p = k + 1
;
ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a
consider b being
set such that A11:
p . (k + 1) = b
;
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 A13:
rng (p | (Seg k)) is
Subset of
(LattPOSet L)
by TARSKI:def 3;
A14:
k <= k + 1
by NAT_1:11;
then
(
len (p | (Seg k)) = k &
p | (Seg k) <> {} )
by A8, A10, CARD_1:27, FINSEQ_1:17;
then consider a being
Element of
(LattPOSet L) such that A15:
for
b being
Element of
(LattPOSet L) st
b in rng (p | (Seg k)) holds
b <= a
by A2, A13;
Seg (k + 1) = dom p
by A10, FINSEQ_1:def 3;
then
k + 1
in dom p
by FINSEQ_1:4;
then
b in rng p
by A11, FUNCT_1:def 3;
then reconsider b =
b as
Element of
(LattPOSet L) by A9;
A16:
(% b) % =
% b
by LATTICE3:def 3
.=
b
by LATTICE3:def 4
;
set a2 =
(% a) "\/" (% b);
(% a) "\/" ((% a) "\/" (% b)) =
((% a) "\/" (% a)) "\/" (% b)
by LATTICES:def 5
.=
(% a) "\/" (% b)
;
then A17:
% a [= (% a) "\/" (% b)
by LATTICES:def 3;
(% b) "\/" ((% a) "\/" (% b)) =
((% b) "\/" (% b)) "\/" (% a)
by LATTICES:def 5
.=
(% b) "\/" (% a)
;
then A18:
% b [= (% a) "\/" (% b)
by LATTICES:def 3;
A19:
(% a) % =
% a
by LATTICE3:def 3
.=
a
by LATTICE3:def 4
;
for
c being
Element of
(LattPOSet L) st
c in X holds
c <= ((% a) "\/" (% b)) %
proof
let c be
Element of
(LattPOSet L);
( c in X implies c <= ((% a) "\/" (% b)) % )
assume A20:
c in X
;
c <= ((% a) "\/" (% b)) %
per cases
( c in rng (p | (Seg k)) or not c in rng (p | (Seg k)) )
;
suppose A22:
not
c in rng (p | (Seg k))
;
c <= ((% a) "\/" (% b)) % consider n being
object such that A23:
n in dom p
and A24:
c = p . n
by A9, A20, FUNCT_1:def 3;
reconsider n =
n as
Element of
NAT by A23;
A25:
n in Seg (k + 1)
by A10, A23, FINSEQ_1:def 3;
A26:
n >= k + 1
proof
assume
not
n >= k + 1
;
contradiction
then A27:
n <= k
by INT_1:7;
1
<= n
by A25, FINSEQ_1:1;
then A28:
n in Seg k
by A27, FINSEQ_1:1;
dom (p | (Seg k)) =
(dom p) /\ (Seg k)
by RELAT_1:61
.=
(Seg (k + 1)) /\ (Seg k)
by A10, FINSEQ_1:def 3
.=
Seg k
by FINSEQ_1:7, NAT_1:11
;
then A29:
(p | (Seg k)) . n = c
by A24, A28, FUNCT_1:47;
n in dom (p | (Seg k))
by A10, A14, A28, FINSEQ_1:17;
hence
contradiction
by A22, A29, FUNCT_1:def 3;
verum
end;
n <= k + 1
by A25, FINSEQ_1:1;
then
c = b
by A11, A24, A26, XXREAL_0:1;
hence
c <= ((% a) "\/" (% b)) %
by A18, A16, LATTICE3:7;
verum end; end;
end;
hence
ex
a being
Element of
(LattPOSet L) st
for
b being
Element of
(LattPOSet L) st
b in X holds
b <= a
;
verum
end; hence
S1[
k + 1]
;
verum end; end;
end;
A30:
S1[ 0 ]
A33:
for k being Nat holds S1[k]
from NAT_1:sch 2(A30, 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
A34:
rng p = X9
by FINSEQ_1:52;
dom p = Seg (len p)
by FINSEQ_1:def 3;
hence
( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
by A33, A34; verum