begin
deffunc H1( LattStr ) -> set = the carrier of $1;
deffunc H2( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_join of $1;
deffunc H3( LattStr ) -> Element of bool [:[: the carrier of $1, the carrier of $1:], the carrier of $1:] = the L_meet of $1;
definition
let X be
set ;
existence
ex b1 being strict LattStr st
( the carrier of b1 = bool X & ( for Y, Z being Subset of X holds
( the L_join of b1 . (Y,Z) = Y \/ Z & the L_meet of b1 . (Y,Z) = Y /\ Z ) ) )
uniqueness
for b1, b2 being strict LattStr st the carrier of b1 = bool X & ( for Y, Z being Subset of X holds
( the L_join of b1 . (Y,Z) = Y \/ Z & the L_meet of b1 . (Y,Z) = Y /\ Z ) ) & the carrier of b2 = bool X & ( for Y, Z being Subset of X holds
( the L_join of b2 . (Y,Z) = Y \/ Z & the L_meet of b2 . (Y,Z) = Y /\ Z ) ) holds
b1 = b2
end;
begin
begin
Lm3:
now for D being non empty set
for f being Function of (bool D),D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds
ex L being strict Lattice st
( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )
let D be non
empty set ;
for f being Function of (bool D),D st ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) holds
ex L being strict Lattice st
( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )let f be
Function of
(bool D),
D;
( ( for a being Element of D holds f . {a} = a ) & ( for X being Subset-Family of D holds f . (f .: X) = f . (union X) ) implies ex L being strict Lattice st
( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) ) )assume that A1:
for
a being
Element of
D holds
f . {a} = a
and A2:
for
X being
Subset-Family of
D holds
f . (f .: X) = f . (union X)
;
ex L being strict Lattice st
( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )defpred S1[
set ,
set ]
means f . {$1,$2} = $2;
consider R being
Relation of
D such that A3:
for
x,
y being
set holds
(
[x,y] in R iff (
x in D &
y in D &
S1[
x,
y] ) )
from RELSET_1:sch 1();
A4:
dom f = bool D
by FUNCT_2:def 1;
A6:
for
x,
y being
Element of
D for
X being
Subset of
D st
y in X holds
f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }
proof
let x,
y be
Element of
D;
for X being Subset of D st y in X holds
f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } let X be
Subset of
D;
( y in X implies f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X } )
assume A7:
y in X
;
f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }
set Y =
{ {t,x} where t is Element of D : t in X } ;
A8:
X \/ {x} = union { {t,x} where t is Element of D : t in X }
proof
thus
X \/ {x} c= union { {t,x} where t is Element of D : t in X }
XBOOLE_0:def 10 union { {t,x} where t is Element of D : t in X } c= X \/ {x}
proof
let s be
set ;
TARSKI:def 3 ( not s in X \/ {x} or s in union { {t,x} where t is Element of D : t in X } )
assume
s in X \/ {x}
;
s in union { {t,x} where t is Element of D : t in X }
then
( (
s in X &
X c= D ) or
s in {x} )
by XBOOLE_0:def 3;
then
( (
s in X &
s is
Element of
D ) or
s = x )
by TARSKI:def 1;
then
( (
s in {s,x} &
{s,x} in { {t,x} where t is Element of D : t in X } ) or (
s in {y,x} &
{y,x} in { {t,x} where t is Element of D : t in X } ) )
by A7, TARSKI:def 2;
hence
s in union { {t,x} where t is Element of D : t in X }
by TARSKI:def 4;
verum
end;
let s be
set ;
TARSKI:def 3 ( not s in union { {t,x} where t is Element of D : t in X } or s in X \/ {x} )
assume
s in union { {t,x} where t is Element of D : t in X }
;
s in X \/ {x}
then consider Z being
set such that A9:
s in Z
and A10:
Z in { {t,x} where t is Element of D : t in X }
by TARSKI:def 4;
consider t being
Element of
D such that A11:
Z = {t,x}
and A12:
t in X
by A10;
(
s = t or (
s = x &
x in {x} ) )
by A9, A11, TARSKI:def 1, TARSKI:def 2;
hence
s in X \/ {x}
by A12, XBOOLE_0:def 3;
verum
end;
{ {t,x} where t is Element of D : t in X } c= bool D
then reconsider Y =
{ {t,x} where t is Element of D : t in X } as
Subset-Family of
D ;
defpred S2[
set ]
means $1
in X;
deffunc H4(
Element of
D)
-> Element of
bool D =
{$1,x};
A13:
bool D c= dom f
by FUNCT_2:def 1;
f .: { H4(t) where t is Element of D : S2[t] } = { (f . H4(t)) where t is Element of D : S2[t] }
from LATTICE3:sch 2(A13);
then
f . (union Y) = f . { (f . {t,x}) where t is Element of D : t in X }
by A2;
hence
f . (X \/ {x}) = f . { (f . {t,x}) where t is Element of D : t in X }
by A8;
verum
end;
A14:
R is_reflexive_in D
A16:
R is_antisymmetric_in D
A19:
R is_transitive_in D
proof
let x,
y,
z be
set ;
RELAT_2:def 8 ( not x in D or not y in D or not z in D or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that A20:
x in D
and A21:
y in D
and A22:
z in D
and A23:
[x,y] in R
and A24:
[y,z] in R
;
[x,z] in R
reconsider a =
x,
b =
y,
c =
z as
Element of
D by A20, A21, A22;
A25:
f . {x,y} = y
by A3, A23;
A26:
f . {y,z} = z
by A3, A24;
then f . {a,c} =
f . {(f . {a}),(f . {b,c})}
by A1
.=
f . ({a} \/ {b,c})
by A5
.=
f . {a,b,c}
by ENUMSET1:2
.=
f . ({a,b} \/ {c})
by ENUMSET1:3
.=
f . {(f . {a,b}),(f . {c})}
by A5
.=
c
by A1, A25, A26
;
hence
[x,z] in R
by A3;
verum
end;
A27:
dom R = D
by A14, ORDERS_1:13;
field R = D
by A14, ORDERS_1:13;
then reconsider R =
R as
Order of
D by A14, A16, A19, A27, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;
set A =
RelStr(#
D,
R #);
RelStr(#
D,
R #) is
complete
proof
let X be
set ;
LATTICE3:def 12 ex a being Element of RelStr(# D,R #) st
( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds
a <= b ) )
reconsider Y =
X /\ D as
Subset of
D by XBOOLE_1:17;
reconsider a =
f . Y as
Element of
RelStr(#
D,
R #) ;
take
a
;
( X is_<=_than a & ( for b being Element of RelStr(# D,R #) st X is_<=_than b holds
a <= b ) )
thus
X is_<=_than a
for b being Element of RelStr(# D,R #) st X is_<=_than b holds
a <= b
let b be
Element of
RelStr(#
D,
R #);
( X is_<=_than b implies a <= b )
assume A28:
X is_<=_than b
;
a <= b
A29:
f . {a,b} =
f . {a,(f . {b})}
by A1
.=
f . (Y \/ {b})
by A5
;
hence
[a,b] in the
InternalRel of
RelStr(#
D,
R #)
by A3;
ORDERS_2:def 5 verum
end;
then reconsider A =
RelStr(#
D,
R #) as non
empty strict complete Poset ;
take L =
latt A;
( H1(L) = D & ( for X being Subset of L holds "\/" X = f . X ) )A34:
(
A is
with_suprema &
A is
with_infima )
by Th12;
then A35:
A = LattPOSet L
by Def15;
hence
H1(
L)
= D
;
for X being Subset of L holds "\/" X = f . Xlet X be
Subset of
L;
"\/" X = f . Xreconsider Y =
X as
Subset of
D by A35;
reconsider a =
f . Y as
Element of
(LattPOSet L) by A34, Def15;
set p =
% a;
X is_<=_than a
then A37:
X is_less_than % a
by Th31;
hence
"\/" X = f . X
by A37, Def21;
verum
end;