Copyright (c) 1996 Association of Mizar Users
environ
vocabulary RELAT_2, ORDERS_1, RELAT_1, WAYBEL_3, LATTICES, LATTICE3, WAYBEL_0,
BOOLE, YELLOW_1, SETFAM_1, BHSP_3, YELLOW_0, QUANTAL1, PRE_TOPC, FUNCT_1,
FILTER_2, SEQM_3, PARTFUN1, CAT_1, GROUP_1, FUNCOP_1, FUNCT_2, CARD_3,
RLVECT_2, WELLORD1, YELLOW_2, FILTER_0, WELLORD2, ORDINAL2, WAYBEL_2,
SUBSET_1, ORDERS_2, WAYBEL_4;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, ORDERS_1,
PRE_TOPC, PARTFUN1, LATTICE3, RELAT_1, RELAT_2, RELSET_1, FUNCT_1,
FUNCT_2, WELLORD1, YELLOW_0, PRE_CIRC, CARD_3, PRALG_1, YELLOW_1, ALG_1,
YELLOW_2, YELLOW_4, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3;
constructors ORDERS_3, PRE_CIRC, TOLER_1, WAYBEL_1, WAYBEL_2, WAYBEL_3,
YELLOW_4, ALG_1;
clusters LATTICE3, RELSET_1, STRUCT_0, WAYBEL_0, WAYBEL_2, WAYBEL_3, YELLOW_1,
YELLOW_2, SUBSET_1, PARTFUN1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions LATTICE3, XBOOLE_0, TARSKI, YELLOW_0, WAYBEL_0, RELAT_1, YELLOW_2,
ORDERS_3;
theorems FUNCOP_1, FUNCT_1, FUNCT_2, LATTICE3, ORDERS_1, ORDERS_3, PARTFUN1,
PRE_TOPC, RELAT_1, RELAT_2, RELSET_1, SETFAM_1, STRUCT_0, TARSKI,
WAYBEL_0, WAYBEL_3, WAYBEL_2, WELLORD1, WELLORD2, YELLOW_0, YELLOW_1,
YELLOW_2, YELLOW_4, ZFMISC_1, XBOOLE_0, XBOOLE_1;
schemes FUNCT_2, PARTFUN1, RELSET_1, YELLOW_2, XBOOLE_0;
begin :: Auxiliary Relations
definition
let L be non empty reflexive RelStr;
canceled;
func L-waybelow -> Relation of L means :Def2:
for x,y being Element of L holds [x,y] in it iff x << y;
existence
proof
defpred P[set,set] means
ex x', y' be Element of L st x' = $1 & y' = $2 & x' << y';
consider R being Relation of the carrier of L, the carrier of L such that
A1: for x,y being set holds [x,y] in R iff x in the carrier of L &
y in the carrier of L & P[x,y] from Rel_On_Set_Ex;
reconsider R as Relation of L ;
take R;
let x,y be Element of L;
hereby assume [x,y] in R;
then consider x', y' being Element of L such that
A2: x' = x & y' = y & x' << y' by A1;
thus x << y by A2;
end;
assume x << y;
hence [x,y] in R by A1;
end;
uniqueness
proof
let A1,A2 be Relation of L;
assume A3: for x,y being Element of L holds [x,y] in A1 iff x << y;
assume A4: for x,y being Element of L holds [x,y] in A2 iff x << y;
thus A1 = A2
proof
let a,b be set;
hereby assume A5: [a,b] in A1;
then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
then reconsider a' = a, b' = b as Element of L;
a' << b' by A3,A5;
hence [a,b] in A2 by A4;
end;
assume A6: [a,b] in A2;
then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
then reconsider a' = a, b' = b as Element of L;
a' << b' by A4,A6;
hence [a,b] in A1 by A3;
end;
end;
end;
definition let L be RelStr;
func IntRel L -> Relation of L equals :Def3:
the InternalRel of L;
coherence ;
correctness;
end;
Lm1:
for L being RelStr, x, y being Element of L holds
[x, y] in IntRel L iff x <= y
proof
let L be RelStr, x, y be Element of L;
hereby assume [x, y] in IntRel L;
then [x, y] in the InternalRel of L by Def3;
hence x <= y by ORDERS_1:def 9;
end;
assume x <= y;
then [x, y] in the InternalRel of L by ORDERS_1:def 9;
hence [x, y] in IntRel L by Def3;
end;
definition let L be RelStr, R be Relation of L;
attr R is auxiliary(i) means :Def4:
for x, y being Element of L holds
[x,y] in R implies x <= y;
attr R is auxiliary(ii) means :Def5:
for x, y, z, u being Element of L holds
( u <= x & [x,y] in R & y <= z implies [u,z] in R );
end;
definition let L be non empty RelStr, R be Relation of L;
attr R is auxiliary(iii) means :Def6:
for x, y, z being Element of L holds
( [x,z] in R & [y,z] in R implies [(x "\/" y),z] in R );
attr R is auxiliary(iv) means :Def7:
for x being Element of L holds [Bottom L,x] in R;
end;
:: Definition 1.9 p.43
definition let L be non empty RelStr, R be Relation of L;
attr R is auxiliary means :Def8:
R is auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv);
end;
definition let L be non empty RelStr;
cluster auxiliary ->
auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;
coherence by Def8;
cluster auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) ->
auxiliary Relation of L;
coherence by Def8;
end;
definition let L be lower-bounded with_suprema transitive antisymmetric RelStr;
cluster auxiliary Relation of L;
existence
proof
set A = IntRel L;
take A;
thus A is auxiliary(i)
proof
let x, y be Element of L;
assume [x,y] in A;
then [x,y] in the InternalRel of L by Def3;
hence thesis by ORDERS_1:def 9;
end;
thus A is auxiliary(ii)
proof
let x, y, z, u be Element of L;
assume that
A1: u <= x and
A2: [x,y] in A and
A3: y <= z;
[x,y] in the InternalRel of L by A2,Def3;
then x <= y by ORDERS_1:def 9;
then u <= y by A1,ORDERS_1:26;
then u <= z by A3,ORDERS_1:26;
then [u,z] in the InternalRel of L by ORDERS_1:def 9;
hence thesis by Def3;
end;
thus A is auxiliary(iii)
proof
let x, y, z be Element of L;
assume that A4: [x,z] in A and A5: [y,z] in A;
[x,z] in the InternalRel of L by A4,Def3;
then A6: x <= z by ORDERS_1:def 9;
[y,z] in the InternalRel of L by A5,Def3;
then A7: y <= z by ORDERS_1:def 9;
ex q being Element of L st x <= q & y <= q &
for c being Element of L st x <= c & y <= c holds q <= c
by LATTICE3:def 10;
then (x "\/" y) <= z by A6,A7,LATTICE3:def 13;
then [x "\/" y, z] in the InternalRel of L by ORDERS_1:def 9;
hence thesis by Def3;
end;
thus A is auxiliary(iv)
proof
let x be Element of L;
Bottom L <= x by YELLOW_0:44;
then [Bottom L,x] in the InternalRel of L by ORDERS_1:def 9;
hence thesis by Def3;
end;
end;
end;
theorem Th1:
for L being lower-bounded sup-Semilattice
for AR being auxiliary(ii) auxiliary(iii) Relation of L
for x, y, z, u being Element of L holds
[x, z] in AR & [y, u] in AR implies [x "\/" y, z "\/" u] in AR
proof
let L be lower-bounded sup-Semilattice;
let AR be auxiliary(ii) auxiliary(iii) Relation of L;
let x,y,z,u be Element of L;
assume
A1: [x, z] in AR & [y, u] in AR;
A2: x <= x & y <= y;
z <= z "\/" u & u <= z "\/" u by YELLOW_0:22;
then [x, z "\/" u] in AR & [y, z "\/" u] in AR by A1,A2,Def5;
hence [x "\/" y, z "\/" u] in AR by Def6;
end;
Lm2:
for L be lower-bounded sup-Semilattice
for AR be auxiliary(i) auxiliary(ii) Relation of L holds
AR is transitive
proof
let L be lower-bounded sup-Semilattice;
let AR be auxiliary(i) auxiliary(ii) Relation of L;
A1: field AR c= (the carrier of L) \/ (the carrier of L) by RELSET_1:19;
now let x,y,z be set;
assume
A2: x in field AR & y in field AR & z in field AR & [x,y] in AR & [y,z] in
AR;
then reconsider x'=x, y'=y, z'=z as Element of L by A1;
reconsider x', y', z' as Element of L;
A3: x' <= y' by A2,Def4;
z' <= z';
hence [x,z] in AR by A2,A3,Def5;
end;
then AR is_transitive_in field AR by RELAT_2:def 8;
hence thesis by RELAT_2:def 16;
end;
definition let L be lower-bounded sup-Semilattice;
cluster auxiliary(i) auxiliary(ii) -> transitive Relation of L;
coherence by Lm2;
end;
definition let L be RelStr;
cluster IntRel L -> auxiliary(i);
coherence
proof
let x, y be Element of L;
assume [x, y] in IntRel L;
hence x <= y by Lm1;
end;
end;
definition let L be transitive RelStr;
cluster IntRel L -> auxiliary(ii);
coherence
proof
set A = IntRel L;
let x,y,z,u be Element of L;
assume that A1: u <= x and A2: [x,y] in A and A3: y <= z;
x <= y by A2,Lm1;
then u <= y by A1,ORDERS_1:26;
then u <= z by A3,ORDERS_1:26;
hence [u,z] in A by Lm1;
end;
end;
definition let L be with_suprema antisymmetric RelStr;
cluster IntRel L -> auxiliary(iii);
coherence
proof
set A = IntRel L;
let x,y,z be Element of L;
assume that A1: [x,z] in A and A2: [y,z] in A;
A3: x <= z by A1,Lm1;
A4: y <= z by A2,Lm1;
ex q being Element of L st x <= q & y <= q &
for c being Element of L st x <= c & y <= c holds q <= c
by LATTICE3:def 10;
then x "\/" y <= z by A3,A4,LATTICE3:def 13;
hence thesis by Lm1;
end;
end;
definition let L be lower-bounded antisymmetric non empty RelStr;
cluster IntRel L -> auxiliary(iv);
coherence
proof
set A = IntRel L;
for x be Element of L holds [Bottom L,x] in A
proof
let x be Element of L;
Bottom L <= x by YELLOW_0:44;
hence thesis by Lm1;
end;
hence A is auxiliary(iv) by Def7;
end;
end;
reserve a for set;
definition let L be lower-bounded sup-Semilattice;
func Aux L means :Def9:
a in it iff a is auxiliary Relation of L;
existence
proof defpred P[set] means $1 is auxiliary Relation of L;
consider X be set such that
A1: for a holds a in X
iff a in bool [:the carrier of L,the carrier of L:] & P[a]
from Separation;
take X;
thus thesis by A1;
end;
uniqueness
proof
let A1,A2 be set such that
A2: a in A1 iff a is auxiliary Relation of L and
A3: a in A2 iff a is auxiliary Relation of L;
thus A1 = A2
proof
thus A1 c= A2
proof
let a; assume a in A1;
then a is auxiliary Relation of L by A2;
hence thesis by A3;
end;
let a; assume a in A2;
then a is auxiliary Relation of L by A3;
hence thesis by A2;
end;
end;
end;
definition let L be lower-bounded sup-Semilattice;
cluster Aux L -> non empty;
coherence
proof
IntRel L is auxiliary Relation of L;
hence thesis by Def9;
end;
end;
Lm3:
for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) Relation of L
for a,b being set st [a,b] in AR holds [a,b] in IntRel L
proof
let L be lower-bounded sup-Semilattice;
let AR be auxiliary(i) Relation of L;
let a,b be set; assume A1: [a,b] in AR;
then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
then reconsider a' = a, b' = b as Element of L;
a' <= b' by A1,Def4;
hence thesis by Lm1;
end;
theorem Th2:
for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) Relation of L holds
AR c= IntRel L
proof
let L be lower-bounded sup-Semilattice;
let AR be auxiliary(i) Relation of L;
let a,b be set; assume [a,b] in AR;
hence thesis by Lm3;
end;
theorem
for L being lower-bounded sup-Semilattice holds
Top InclPoset Aux L = IntRel L
proof
let L be lower-bounded sup-Semilattice;
IntRel L = "/\"({},InclPoset Aux L)
proof
set P = InclPoset Aux L;
set I = IntRel L;
I in Aux L by Def9;
then I in the carrier of P by YELLOW_1:1;
then reconsider I as Element of P;
A1: I is_<=_than {} by YELLOW_0:6;
for b being Element of P st b is_<=_than {} holds I >= b
proof
let b be Element of P;
b in the carrier of InclPoset Aux L;
then b in Aux L by YELLOW_1:1;
then reconsider b' = b as auxiliary Relation of L by Def9;
assume b is_<=_than {};
b' c= I by Th2;
hence thesis by YELLOW_1:3;
end;
hence thesis by A1,YELLOW_0:31;
end;
hence thesis by YELLOW_0:def 12;
end;
definition let L be lower-bounded sup-Semilattice;
cluster InclPoset Aux L -> upper-bounded;
coherence
proof
set I = IntRel L;
I in Aux L by Def9;
then I in the carrier of InclPoset Aux L by YELLOW_1:1;
then reconsider I as Element of InclPoset Aux L;
take I;
I is_>=_than the carrier of InclPoset Aux L
proof
let b be Element of InclPoset Aux L;
assume b in the carrier of InclPoset Aux L;
then b in Aux L by YELLOW_1:1;
then reconsider b' = b as auxiliary Relation of L by Def9;
b' c= I by Th2;
hence thesis by YELLOW_1:3;
end;
hence thesis;
end;
end;
definition let L be non empty RelStr;
func AuxBottom L -> Relation of L means :Def10:
for x,y be Element of L holds [x,y] in it iff x = Bottom L;
existence
proof defpred P[set,set] means $1 = Bottom L;
consider R being Relation of the carrier of L, the carrier of L such that
A1: for a,b be set holds [a,b] in R iff a in the carrier of L &
b in the carrier of L & P[a,b] from Rel_On_Set_Ex;
reconsider R as Relation of L ;
take R;
let x,y be Element of L;
thus [x,y] in R implies x = Bottom L by A1;
assume x = Bottom L;
hence [x,y] in R by A1;
end;
uniqueness
proof
let A1,A2 be Relation of L;
assume A2: for x,y be Element of L holds [x,y] in A1 iff x = Bottom L;
assume A3: for x,y be Element of L holds [x,y] in A2 iff x = Bottom L;
thus A1 = A2
proof
let a,b be set;
hereby assume A4: [a,b] in A1;
then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
then reconsider a' = a, b' = b as Element of L;
[a',b'] in A1 by A4;
then a' = Bottom L by A2;
then [a',b'] in A2 by A3;
hence [a,b] in A2;
end;
assume A5: [a,b] in A2;
then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
then reconsider a' = a, b' = b as Element of L;
[a',b'] in A2 by A5;
then a' = Bottom L by A3;
then [a',b'] in A1 by A2;
hence [a,b] in A1;
end;
end;
end;
definition let L be lower-bounded sup-Semilattice;
cluster AuxBottom L -> auxiliary;
coherence
proof
set A = AuxBottom L;
A1:A is auxiliary(i)
proof
let x, y be Element of L;
assume [x,y] in A;
then x = Bottom L by Def10;
hence thesis by YELLOW_0:44;
end;
A2:A is auxiliary(ii)
proof let x, y, z, u be Element of L;
assume A3: u <= x & [x,y] in A & y <= z;
then A4: x = Bottom L by Def10;
Bottom L <= u by YELLOW_0:44;
then u = Bottom L by A3,A4,ORDERS_1:25;
hence thesis by Def10;
end;
A5:A is auxiliary(iii)
proof
let x, y, z be Element of L;
assume [x,z] in A & [y,z] in A;
then A6: x = Bottom L & y = Bottom L by Def10;
then x <= y;
then x "\/" y = Bottom L by A6,YELLOW_0:24;
hence thesis by Def10;
end;
for x be Element of L holds [Bottom L,x] in A by Def10;
then A is auxiliary(iv) by Def7;
hence thesis by A1,A2,A5,Def8;
end;
end;
theorem Th4:
for L being lower-bounded sup-Semilattice
for AR being auxiliary(iv) Relation of L holds AuxBottom L c= AR
proof
let L be with_suprema lower-bounded Poset;
let AR be auxiliary(iv) Relation of L;
let a,b be set;
assume A1: [a,b] in AuxBottom L;
then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
then reconsider a' = a, b' = b as Element of L;
[a',b'] in AuxBottom L by A1;
then a' = Bottom L by Def10;
then [a',b'] in AR by Def7;
hence [a,b] in AR;
end;
theorem
for L being lower-bounded sup-Semilattice
for AR being auxiliary(iv) Relation of L holds
Bottom InclPoset Aux L = AuxBottom L
proof
let L be with_suprema lower-bounded Poset;
let AR be auxiliary(iv) Relation of L;
AuxBottom L in Aux L by Def9;
then AuxBottom L in the carrier of InclPoset Aux L by YELLOW_1:1;
then reconsider N = AuxBottom L as Element of InclPoset Aux L;
AuxBottom L = "\/"({},InclPoset Aux L)
proof
A1: N is_>=_than {} by YELLOW_0:6;
for b being Element of InclPoset Aux L st b is_>=_than {} holds N <= b
proof
let b be Element of InclPoset Aux L;
assume b is_>=_than {};
b in the carrier of InclPoset Aux L;
then b in Aux L by YELLOW_1:1;
then reconsider b' = b as auxiliary Relation of L by Def9;
N c= b' by Th4;
hence thesis by YELLOW_1:3;
end;
hence thesis by A1,YELLOW_0:30;
end;
hence thesis by YELLOW_0:def 11;
end;
definition let L be lower-bounded sup-Semilattice;
cluster InclPoset Aux L -> lower-bounded;
coherence
proof
set I = AuxBottom L;
I in Aux L by Def9;
then I in the carrier of InclPoset Aux L by YELLOW_1:1;
then reconsider I as Element of InclPoset Aux L;
take I;
I is_<=_than the carrier of InclPoset Aux L
proof
let b be Element of InclPoset Aux L;
assume b in the carrier of InclPoset Aux L;
then b in Aux L by YELLOW_1:1;
then reconsider b' = b as auxiliary Relation of L by Def9;
I c= b' by Th4;
hence thesis by YELLOW_1:3;
end;
hence thesis;
end;
end;
theorem Th6:
for L being lower-bounded sup-Semilattice
for a,b being auxiliary(i) Relation of L holds
a /\ b is auxiliary(i) Relation of L
proof
let L be with_suprema lower-bounded Poset;
let a,b be auxiliary(i) Relation of L;
reconsider ab = a /\ b as Relation of L ;
for x, y be Element of L holds [x,y] in ab implies x <= y
proof
let x, y be Element of L;
assume [x,y] in ab;
then [x,y] in a & [x,y] in b by XBOOLE_0:def 3;
hence x <= y by Def4;
end;
hence thesis by Def4;
end;
theorem Th7:
for L being lower-bounded sup-Semilattice
for a,b being auxiliary(ii) Relation of L holds
a /\ b is auxiliary(ii) Relation of L
proof
let L be with_suprema lower-bounded Poset;
let a,b be auxiliary(ii) Relation of L;
reconsider ab = a /\ b as Relation of L ;
for x, y, z, u be Element of L holds
u <= x & [x,y] in ab & y <= z implies [u,z] in ab
proof
let x, y, z, u be Element of L;
assume A1: u <= x & [x,y] in ab & y <= z;
then [x,y] in a & [x,y] in b by XBOOLE_0:def 3;
then [u,z] in a & [u,z] in b by A1,Def5;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis by Def5;
end;
theorem Th8:
for L being lower-bounded sup-Semilattice
for a,b being auxiliary(iii) Relation of L holds
a /\ b is auxiliary(iii) Relation of L
proof
let L be with_suprema lower-bounded Poset;
let a,b be auxiliary(iii) Relation of L;
reconsider ab = a /\ b as Relation of L ;
for x, y, z be Element of L holds
[x,z] in ab & [y,z] in ab implies [(x "\/" y),z] in ab
proof
let x, y, z be Element of L;
assume [x,z] in ab & [y,z] in ab;
then [x,z] in a & [x,z] in b & [y,z] in a & [y,z] in b by XBOOLE_0:def 3;
then [(x "\/" y),z] in a & [(x "\/" y),z] in b by Def6;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis by Def6;
end;
theorem Th9:
for L being lower-bounded sup-Semilattice
for a,b being auxiliary(iv) Relation of L holds
a /\ b is auxiliary(iv) Relation of L
proof
let L be with_suprema lower-bounded Poset;
let a,b be auxiliary(iv) Relation of L;
reconsider ab = a /\ b as Relation of L ;
for x be Element of L holds [Bottom L,x] in ab
proof
let x be Element of L;
[Bottom L,x] in a & [Bottom L,x] in b by Def7;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis by Def7;
end;
theorem Th10:
for L being lower-bounded sup-Semilattice
for a,b being auxiliary Relation of L holds
a /\ b is auxiliary Relation of L
proof
let L be with_suprema lower-bounded Poset;
let a,b be auxiliary Relation of L;
reconsider ab = a /\ b as Relation of L ;
ab is auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv)
by Th6,Th7,Th8,Th9;
hence thesis by Def8;
end;
theorem Th11:
for L being lower-bounded sup-Semilattice
for X being non empty Subset of InclPoset Aux L holds
meet X is auxiliary Relation of L
proof
let L be with_suprema lower-bounded Poset;
let X be non empty Subset of InclPoset Aux L;
X c= the carrier of InclPoset Aux L;
then A1: X c= Aux L by YELLOW_1:1;
consider a be Element of X;
a in X;
then a is auxiliary Relation of L by A1,Def9;
then meet X c= [:the carrier of L,the carrier of L:] by SETFAM_1:8;
then meet X is Relation of the carrier of L by RELSET_1:def 1;
then reconsider ab = meet X as Relation of L ;
now
thus ab is auxiliary(i)
proof
let x, y be Element of L;
assume A2: [x,y] in ab;
consider V be Element of X;
A3: V in X;
A4: [x,y] in V by A2,SETFAM_1:def 1;
V is auxiliary Relation of L by A1,A3,Def9;
hence x <= y by A4,Def4;
end;
thus ab is auxiliary(ii)
proof
let x, y, z, u be Element of L;
assume A5: u <= x & [x,y] in ab & y <= z;
for Y be set st Y in X holds [u,z] in Y
proof
let Y be set; assume A6: Y in X;
then A7: Y is auxiliary Relation of L by A1,Def9;
[x,y] in Y by A5,A6,SETFAM_1:def 1;
hence thesis by A5,A7,Def5;
end;
hence thesis by SETFAM_1:def 1;
end;
thus ab is auxiliary(iii)
proof
let x, y, z be Element of L;
assume A8: [x,z] in ab & [y,z] in ab;
for Y be set st Y in X holds [(x "\/" y),z] in Y
proof
let Y be set; assume A9: Y in X;
then A10: Y is auxiliary Relation of L by A1,Def9;
[x,z] in Y & [y,z] in Y by A8,A9,SETFAM_1:def 1;
hence thesis by A10,Def6;
end;
hence thesis by SETFAM_1:def 1;
end;
thus ab is auxiliary(iv)
proof
let x be Element of L;
for Y be set st Y in X holds [Bottom L,x] in Y
proof
let Y be set; assume Y in X;
then Y is auxiliary Relation of L by A1,Def9;
hence thesis by Def7;
end;
hence thesis by SETFAM_1:def 1;
end;
end;
hence thesis by Def8;
end;
definition let L be lower-bounded sup-Semilattice;
cluster InclPoset Aux L -> with_infima;
coherence
proof
for x, y be set st (x in Aux L & y in Aux L) holds x /\ y in Aux L
proof
let x, y be set;
assume x in Aux L & y in Aux L;
then x is auxiliary Relation of L & y is auxiliary Relation of L by Def9;
then x /\ y is auxiliary Relation of L by Th10;
hence x /\ y in Aux L by Def9;
end;
hence InclPoset Aux L is with_infima by YELLOW_1:12;
end;
end;
definition let L be lower-bounded sup-Semilattice;
cluster InclPoset Aux L -> complete;
coherence
proof
for X be Subset of InclPoset Aux L holds ex_inf_of X, InclPoset Aux L
proof
let X be Subset of InclPoset Aux L;
set N = meet X;
per cases;
suppose A1: X <> {};
then N is auxiliary Relation of L by Th11;
then N in Aux L by Def9;
then N in the carrier of InclPoset Aux L by YELLOW_1:1;
then reconsider N as Element of InclPoset Aux L;
A2: X is_>=_than N
proof
let b be Element of InclPoset Aux L;
assume b in X;
then N c= b by SETFAM_1:4;
hence N <= b by YELLOW_1:3;
end;
for b being Element of InclPoset Aux L st X is_>=_than b holds N >= b
proof
let b be Element of InclPoset Aux L;
assume A3: X is_>=_than b;
for Z1 be set st Z1 in X holds b c= Z1
proof
let Z1 be set; assume A4: Z1 in X;
then reconsider Z1' = Z1 as Element of InclPoset Aux L;
b <= Z1' by A3,A4,LATTICE3:def 8;
hence b c= Z1 by YELLOW_1:3;
end;
then b c= meet X by A1,SETFAM_1:6;
hence thesis by YELLOW_1:3;
end;
hence thesis by A2,YELLOW_0:16;
suppose X = {};
hence thesis by YELLOW_0:43;
end;
hence thesis by YELLOW_2:30;
end;
end;
definition let L be non empty RelStr, x be Element of L;
let AR be Relation of the carrier of L;
A1: {y where y is Element of L : [y,x] in AR} c= the carrier of L
proof let z be set; assume z in {y where y is Element of L: [y,x] in AR};
then ex y being Element of L st z = y & [y,x] in AR;
hence thesis;
end;
func AR-below x -> Subset of L equals :Def11:
{y where y is Element of L: [y,x] in AR};
correctness by A1;
A2: {y where y is Element of L: [x,y] in AR} c= the carrier of L
proof let z be set; assume z in {y where y is Element of L: [x,y] in AR};
then ex y being Element of L st z = y & [x,y] in AR;
hence thesis;
end;
func AR-above x -> Subset of L equals :Def12:
{y where y is Element of L: [x,y] in AR};
correctness by A2;
end;
theorem Th12:
for L being lower-bounded sup-Semilattice, x being Element of L
for AR being auxiliary(i) Relation of L holds
AR-below x c= downarrow x
proof
let L be lower-bounded sup-Semilattice, x be Element of L,
AR be auxiliary(i) Relation of L;
let a;
A1:AR-below x = {y where y is Element of L: [y,x] in AR} by Def11;
assume a in AR-below x;
then consider y1 be Element of L such that A2: y1 = a & [y1,x] in AR by A1;
y1 <= x by A2,Def4;
hence thesis by A2,WAYBEL_0:17;
end;
definition let L be lower-bounded sup-Semilattice, x be Element of L;
let AR be auxiliary(iv) Relation of L;
cluster AR-below x -> non empty;
coherence
proof
set I = AR-below x;
A1:I = {y where y is Element of L: [y,x] in AR} by Def11;
[Bottom L,x] in AR by Def7;
then Bottom L in I by A1;
hence thesis;
end;
end;
definition let L be lower-bounded sup-Semilattice, x be Element of L;
let AR be auxiliary(ii) Relation of L;
cluster AR-below x -> lower;
coherence
proof
set I = AR-below x;
A1:I = {y where y is Element of L: [y,x] in AR} by Def11;
let x1, y1 be Element of L;
assume A2: x1 in I & y1 <= x1;
then consider v1 be Element of L such that A3: v1 = x1 & [v1, x] in AR by
A1;
x <= x;
then [y1, x] in AR by A2,A3,Def5;
hence thesis by A1;
end;
end;
definition let L be lower-bounded sup-Semilattice, x be Element of L;
let AR be auxiliary(iii) Relation of L;
cluster AR-below x -> directed;
coherence
proof
set I = AR-below x;
A1:I = {y where y is Element of L: [y,x] in AR} by Def11;
let u1,u2 be Element of L; assume A2: u1 in I & u2 in I;
then consider v1 be Element of L such that A3: v1 = u1 &
[v1,x] in AR by A1;
consider v2 be Element of L such that A4: v2 = u2 &
[v2,x] in AR by A1,A2;
take u12 = u1 "\/" u2;
[u12,x] in AR by A3,A4,Def6;
hence thesis by A1,YELLOW_0:22;
end;
end;
definition let L be lower-bounded sup-Semilattice;
let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;
func AR-below -> map of L, InclPoset Ids L means :Def13:
for x be Element of L holds
it.x = AR-below x;
existence
proof
deffunc F(Element of L) = AR-below $1;
A1: for x being Element of L holds F(x) is Element of InclPoset Ids L
proof
let x be Element of L;
reconsider I = F(x) as Ideal of L;
I in {X where X is Ideal of L: not contradiction};
then I in Ids L by WAYBEL_0:def 23;
then I in the carrier of InclPoset Ids L by YELLOW_1:1;
hence thesis;
end;
consider f being map of L, InclPoset Ids L such that
A2: for x being Element of L holds f.x = F(x) from KappaMD(A1);
take f;
thus thesis by A2;
end;
uniqueness
proof
let M1, M2 be map of L, InclPoset Ids L;
assume A3: for x be Element of L holds M1.x = AR-below x;
assume A4: for x be Element of L holds M2.x = AR-below x;
for x be set st x in the carrier of L holds M1.x = M2.x
proof
let x be set; assume x in the carrier of L;
then reconsider x' = x as Element of L;
thus M1.x = AR-below x' by A3
.= M2.x by A4;
end;
hence thesis by FUNCT_2:18;
end;
end;
theorem Th13:
for L being non empty RelStr, AR being Relation of L
for a being set, y being Element of L holds
a in AR-below y iff [a,y] in AR
proof
let L be non empty RelStr, AR be Relation of L;
let a be set, y be Element of L;
A1: AR-below y = {z where z is Element of L: [z,y] in AR} by Def11;
a in AR-below y iff [a,y] in AR
proof
hereby assume a in AR-below y;
then consider z being Element of L such that A2: a = z & [z,y] in AR by A1
;
thus [a,y] in AR by A2;
end;
assume A3: [a,y] in AR;
then a in the carrier of L by ZFMISC_1:106;
then reconsider x' = a as Element of L;
ex z being Element of L st a = z & [z,y] in AR
proof
take x';
thus thesis by A3;
end;
hence a in AR-below y by A1;
end;
hence thesis;
end;
theorem
for L being sup-Semilattice, AR being Relation of L
for y being Element of L holds
a in AR-above y iff [y,a] in AR
proof
let L be with_suprema Poset, AR be Relation of L;
let y be Element of L;
A1: AR-above y = {z where z is Element of L: [y,z] in AR} by Def12;
a in AR-above y iff [y,a] in AR
proof
hereby assume a in AR-above y;
then consider z being Element of L such that A2: a = z & [y,z] in AR by A1
;
thus [y,a] in AR by A2;
end;
assume A3: [y,a] in AR;
then a in the carrier of L by ZFMISC_1:106;
then reconsider x' = a as Element of L;
ex z being Element of L st a = z & [y,z] in AR
proof
take x';
thus thesis by A3;
end;
hence a in AR-above y by A1;
end;
hence thesis;
end;
Lm4:
for L be with_suprema lower-bounded Poset, AR be Relation of L
for a be set, y be Element of L holds
a in downarrow y iff [a,y] in the InternalRel of L
proof
let L be with_suprema lower-bounded Poset, AR be Relation of L;
let a be set, y be Element of L;
hereby assume A1: a in downarrow y;
then reconsider a' = a as Element of L;
a' <= y by A1,WAYBEL_0:17;
hence [a,y] in the InternalRel of L by ORDERS_1:def 9;
end;
assume A2: [a,y] in the InternalRel of L;
then a in the carrier of L by ZFMISC_1:106;
then reconsider a' = a as Element of L;
a' <= y by A2,ORDERS_1:def 9;
hence thesis by WAYBEL_0:17;
end;
theorem
for L being lower-bounded sup-Semilattice, AR being auxiliary(i) Relation of
L
for x being Element of L holds
AR = the InternalRel of L implies AR-below x = downarrow x
proof
let L be lower-bounded sup-Semilattice, AR be auxiliary(i) Relation of L;
let x be Element of L;
assume A1: AR = the InternalRel of L;
thus AR-below x c= downarrow x by Th12;
thus downarrow x c= AR-below x
proof
let a; assume a in downarrow x;
then [a,x] in AR by A1,Lm4;
hence thesis by Th13;
end;
end;
definition let L be non empty Poset;
func MonSet L -> strict RelStr means :Def14:
( a in the carrier of it iff
ex s be map of L, InclPoset Ids L st a = s & s is monotone &
for x be Element of L holds s.x c= downarrow x ) &
for c, d be set holds [c,d] in the InternalRel of it iff
ex f,g be map of L, InclPoset Ids L st c = f & d = g &
c in the carrier of it & d in the carrier of it & f <= g;
existence
proof defpred P[set] means
ex s be map of L, InclPoset Ids L st $1 = s &
s is monotone &
for x be Element of L holds s.x c= downarrow x;
consider S be set such that
A1: a in S iff a in PFuncs (the carrier of L, the carrier of
InclPoset Ids L) & P[a] from Separation;
A2: a in S iff
ex s be map of L, InclPoset Ids L st a = s &
s is monotone &
for x be Element of L holds s.x c= downarrow x
proof
thus a in S implies
ex s be map of L, InclPoset Ids L st a = s &
s is monotone &
for x be Element of L holds s.x c= downarrow x by A1;
given s be map of L, InclPoset Ids L such that
A3: a = s & s is monotone & for x be Element of L holds s.x c= downarrow x;
s in PFuncs (the carrier of L, the carrier of
InclPoset Ids L) by PARTFUN1:119;
hence a in S by A1,A3;
end;
defpred P[set,set] means
ex f,g be map of L, InclPoset Ids L st $1 = f & $2 = g & f <= g;
consider R be Relation of S, S such that
A4: for c, d be set holds [c,d] in R iff c in S & d in S & P[c,d]
from Rel_On_Set_Ex;
A5: for c, d be set holds [c,d] in R iff ex f,g be map of L,
InclPoset Ids L st c = f & d = g &
c in S & d in S & f <= g
proof
let c,d be set;
hereby assume A6: [c,d] in R;
then A7: c in S & d in S by A4;
consider f,g be map of L,
InclPoset Ids L such that A8: c = f & d = g & f <= g
by A4,A6;
thus ex f,g be map of L, InclPoset Ids L st
c = f & d = g & c in S & d in S & f <= g by A7,A8;
end;
given f,g be map of L, InclPoset Ids L such that
A9: c = f & d = g & c in S & d in S & f <= g;
thus [c,d] in R by A4,A9;
end;
take RelStr (#S,R#);
thus thesis by A2,A5;
end;
uniqueness
proof
let R1, R2 be strict RelStr;
assume A10: ( a in the carrier of R1 iff
ex s be map of L, InclPoset Ids L st a = s &
s is monotone &
for x be Element of L holds s.x c= downarrow x ) &
for c, d be set holds [c,d] in the InternalRel of R1 iff
ex f,g be map of L, InclPoset Ids L st
c = f & d = g & c in the carrier of R1 & d in the carrier of R1 &
f <= g;
assume A11: ( a in the carrier of R2 iff
ex s be map of L, InclPoset Ids L st a = s &
s is monotone &
for x be Element of L holds s.x c= downarrow x ) &
for c, d be set holds [c,d] in the InternalRel of R2 iff
ex f,g be map of L, InclPoset Ids L st
c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g;
A12: the carrier of R1 = the carrier of R2
proof
thus the carrier of R1 c= the carrier of R2
proof
let b be set; assume b in the carrier of R1;
then consider s be map of L, InclPoset Ids L such that
A13: b = s & s is monotone &
for x be Element of L holds s.x c= downarrow x by A10;
thus b in the carrier of R2 by A11,A13;
end;
thus the carrier of R2 c= the carrier of R1
proof
let b be set; assume b in the carrier of R2;
then consider s be map of L, InclPoset Ids L such that
A14: b = s & s is monotone &
for x be Element of L holds s.x c= downarrow x by A11;
thus b in the carrier of R1 by A10,A14;
end;
end;
the InternalRel of R1 = the InternalRel of R2
proof
let c,d be set;
A15: now assume [c,d] in the InternalRel of R1;
then consider f,g be map of L, InclPoset Ids L such that
A16: c = f & d = g & c in the carrier of R1 & d in the carrier of R1 &
f <= g by A10;
thus [c,d] in the InternalRel of R2 by A11,A12,A16;
end;
now assume [c,d] in the InternalRel of R2;
then consider f,g be map of L, InclPoset Ids L such that
A17: c = f & d = g & c in the carrier of R2 & d in the carrier of R2 &
f <= g by A11;
thus [c,d] in the InternalRel of R1 by A10,A12,A17;
end; hence thesis by A15;
end;
hence thesis by A12;
end;
end;
theorem
for L being lower-bounded sup-Semilattice holds
MonSet L is full SubRelStr of (InclPoset Ids L)|^(the carrier of L)
proof
let L be lower-bounded sup-Semilattice;
set J = ((the carrier of L) --> InclPoset Ids L);
A1: the carrier of MonSet L c=
the carrier of (InclPoset Ids L)|^(the carrier of L)
proof
let a be set; assume a in the carrier of MonSet L;
then consider s be map of L, InclPoset Ids L such that
A2: a = s & s is monotone &
for x be Element of L holds s.x c= downarrow x by Def14;
s in Funcs (the carrier of L, the carrier of InclPoset Ids L)
by FUNCT_2:11;
hence thesis by A2,YELLOW_1:28;
end;
A3:the InternalRel of MonSet L c=
the InternalRel of (InclPoset Ids L)|^(the carrier of L)
proof
let a,b be set; assume [a,b] in the InternalRel of MonSet L;
then consider f,g be map of L, InclPoset Ids L such that
A4: a = f & b = g & a in the carrier of MonSet L &
b in the carrier of MonSet L & f <= g by Def14;
set AG = product ((the carrier of L) --> InclPoset Ids L);
A5: AG = ((InclPoset Ids L) |^ the carrier of L) by YELLOW_1:def 5;
A6: f in Funcs (the carrier of L, the carrier of InclPoset Ids L) &
g in Funcs (the carrier of L, the carrier of InclPoset Ids L)
by FUNCT_2:11;
then A7: f in the carrier of AG & g in the carrier of AG by A5,YELLOW_1:28;
reconsider f' = f, g' = g as Element of AG
by A5,A6,YELLOW_1:28;
A8: f' in product Carrier ((the carrier of L) --> InclPoset Ids L)
by A7,YELLOW_1:def 4;
ex ff,gg being Function st ff = f' & gg = g' &
for i be set st i in the carrier of L
ex R being RelStr, xi,yi being Element of R
st R = J.i & xi = ff.i & yi = gg.i & xi <= yi
proof
take f,g;
thus f = f' & g = g';
let i be set; assume A9: i in the carrier of L;
then reconsider i' = i as Element of L;
take R = InclPoset Ids L;
reconsider xi = f.i', yi = g.i' as Element of R;
take xi, yi;
thus R = J.i & xi = f.i & yi = g.i by A9,FUNCOP_1:13;
reconsider i' = i as Element of L by A9;
consider a, b be Element of InclPoset Ids L such that
A10: a = f.i' & b = g.i' & a <= b by A4,YELLOW_2:def 1;
thus thesis by A10;
end;
then f' <= g' by A8,YELLOW_1:def 4;
then [a,b] in the InternalRel of
product ((the carrier of L) --> InclPoset Ids L)
by A4,ORDERS_1:def 9;
hence thesis by YELLOW_1:def 5;
end;
set J = ((the carrier of L) --> InclPoset Ids L);
the InternalRel of MonSet L =
(the InternalRel of (InclPoset Ids L)|^(the carrier of L) )|_2
the carrier of MonSet L
proof
let a,b be set;
thus [a,b] in the InternalRel of MonSet L implies
[a,b] in (the InternalRel of (InclPoset Ids L)|^(the carrier of L))|_2
the carrier of MonSet L by A3,WELLORD1:16;
assume [a,b] in (the InternalRel of (InclPoset Ids L)|^
(the carrier of L) )|_2 the carrier of MonSet L;
then A11: [a,b] in (the InternalRel of (InclPoset Ids L)|^
(the carrier of L) ) &
[a,b] in [:the carrier of MonSet L, the carrier of MonSet L:]
by WELLORD1:16;
then A12: a in the carrier of (InclPoset Ids L)|^(the carrier of L) &
b in the carrier of (InclPoset Ids L)|^(the carrier of L)
by ZFMISC_1:106;
then A13: a in the carrier of product J & b in the carrier of product J
by YELLOW_1:def 5;
reconsider a' = a, b' = b as Element of product J
by A12,YELLOW_1:def 5;
[a',b'] in (the InternalRel of product J) by A11,YELLOW_1:def 5;
then A14: a' <= b' by ORDERS_1:def 9;
a' in product Carrier J by A13,YELLOW_1:def 4;
then consider f,g being Function such that
A15: f = a' & g = b' &
for i be set st i in the carrier of L
ex R being RelStr, xi,yi being Element of R
st R = ((the carrier of L) --> InclPoset Ids L).i &
xi = f.i & yi = g.i & xi <= yi by A14,YELLOW_1:def 4;
f in Funcs (the carrier of L, the carrier of InclPoset Ids L) &
g in Funcs (the carrier of L, the carrier of InclPoset Ids L)
by A12,A15,YELLOW_1:28;
then reconsider f, g as Function of the carrier of L,
the carrier of InclPoset Ids L by FUNCT_2:121;
reconsider f, g as map of L, InclPoset Ids L ;
now take f, g;
f <= g
proof
let j be set; assume j in the carrier of L;
then reconsider j' = j as Element of L;
take f.j', g.j';
consider R being RelStr, xi,yi being Element of R such that
A16: R = ((the carrier of L) --> InclPoset Ids L).j' &
xi = f.j' & yi = g.j' & xi <= yi by A15;
thus thesis by A16,FUNCOP_1:13;
end;
hence a' = f & b' = g & a' in the carrier of MonSet L &
b' in the carrier of MonSet L & f <= g by A11,A15,ZFMISC_1:106;
end;
hence [a,b] in the InternalRel of MonSet L by Def14;
end;
hence MonSet L is full SubRelStr of
(InclPoset Ids L)|^(the carrier of L) by A1,A3,YELLOW_0:def 13,def 14;
end;
theorem Th17:
for L being lower-bounded sup-Semilattice,
AR being auxiliary(ii) Relation of L
for x, y being Element of L holds
x <= y implies AR-below x c= AR-below y
proof
let L be lower-bounded sup-Semilattice, AR be auxiliary(ii) Relation of L;
let x, y be Element of L;
assume A1: x <= y;
A2:AR-below x = {y1 where y1 is Element of L: [y1,x] in AR} by Def11;
let a; assume a in AR-below x;
then consider y2 be Element of L such that A3: y2 = a & [y2,x] in AR by A2;
y2 <= y2;
then [y2,y] in AR by A1,A3,Def5;
hence thesis by A3,Th13;
end;
definition let L be lower-bounded sup-Semilattice;
let AR be auxiliary(ii) auxiliary(iii) auxiliary(iv) Relation of L;
cluster AR-below -> monotone;
coherence
proof
set s = AR-below;
let x, y be Element of L;
A1: s.x = AR-below x & s.y = AR-below y by Def13;
assume x <= y;
then AR-below x c= AR-below y by Th17;
hence thesis by A1,YELLOW_1:3;
end;
end;
theorem Th18:
for L being lower-bounded sup-Semilattice, AR being auxiliary Relation of L
holds
AR-below in the carrier of MonSet L
proof
let L be lower-bounded sup-Semilattice, AR be auxiliary Relation of L;
set s = AR-below;
ex s be map of L, InclPoset Ids L st
AR-below = s & s is monotone &
for x be Element of L holds s.x c= downarrow x
proof
take s;
for x be Element of L holds s.x c= downarrow x
proof
let x be Element of L;
s.x = AR-below x by Def13;
hence s.x c= downarrow x by Th12;
end;
hence thesis;
end;
hence thesis by Def14;
end;
definition let L be lower-bounded sup-Semilattice;
cluster MonSet L -> non empty;
coherence
proof
consider AR be auxiliary Relation of L;
AR-below in the carrier of MonSet L by Th18;
hence thesis by STRUCT_0:def 1;
end;
end;
theorem Th19:
for L being lower-bounded sup-Semilattice holds
IdsMap L in the carrier of MonSet L
proof
let L be lower-bounded sup-Semilattice;
set s = IdsMap L;
ex s' be map of L, InclPoset Ids L st
s = s' & s' is monotone & for x be Element of L holds s'.x c= downarrow x
proof
take s;
thus thesis by YELLOW_2:def 4;
end;
hence thesis by Def14;
end;
theorem
for L being lower-bounded sup-Semilattice, AR being auxiliary Relation of L
holds
AR-below <= IdsMap L
proof
let L be lower-bounded sup-Semilattice, AR be auxiliary Relation of L;
let x be set;
assume x in the carrier of L;
then reconsider x' = x as Element of L;
A1: (AR-below).x' = AR-below x' by Def13;
(IdsMap L).x' = downarrow x' by YELLOW_2:def 4;
then A2: (AR-below).x c= (IdsMap L).x by A1,Th12;
reconsider a = (AR-below).x',
b = (IdsMap L).x' as Element of InclPoset Ids L;
take a, b;
thus thesis by A2,YELLOW_1:3;
end;
theorem Th21:
for L being lower-bounded non empty Poset
for I being Ideal of L holds Bottom L in I
proof
let L be lower-bounded non empty Poset;
let I be Ideal of L;
consider x be Element of I;
Bottom L <= x by YELLOW_0:44;
hence thesis by WAYBEL_0:def 19;
end;
theorem
for L being upper-bounded non empty Poset
for F being Filter of L holds Top L in F
proof
let L be upper-bounded non empty Poset;
let F be Filter of L;
consider x be Element of F;
Top L >= x by YELLOW_0:45;
hence thesis by WAYBEL_0:def 20;
end;
theorem Th23:
for L being lower-bounded non empty Poset holds
downarrow Bottom L = {Bottom L}
proof
let L be lower-bounded non empty Poset;
thus downarrow Bottom L c= {Bottom L}
proof
let a; assume a in downarrow Bottom L;
then a in downarrow {Bottom L} by WAYBEL_0:def 17;
then a in {x where x is Element of L : ex y being Element of L st x <= y &
y in {Bottom L}} by WAYBEL_0:14;
then consider a' be Element of L such that A1: a' = a &
ex y being Element of L st a' <= y & y in {Bottom L};
consider y being Element of L such that A2: a' <= y & y in {Bottom
L} by A1;
A3: Bottom L <= a' by YELLOW_0:44;
y = Bottom L by A2,TARSKI:def 1;
hence thesis by A1,A2,A3,ORDERS_1:25;
end;
let a; assume a in {Bottom L};
then A4: a = Bottom L by TARSKI:def 1;
Bottom L <= Bottom L;
hence thesis by A4,WAYBEL_0:17;
end;
theorem
for L being upper-bounded non empty Poset holds uparrow Top L = {Top L}
proof let L be upper-bounded non empty Poset;
thus uparrow Top L c= {Top L}
proof
let x be set; assume
A1: x in uparrow Top L;
then reconsider x as Element of L;
x >= Top L & x <= Top L by A1,WAYBEL_0:18,YELLOW_0:45;
then x = Top L by ORDERS_1:25;
hence thesis by TARSKI:def 1;
end;
let x be set; assume x in {Top L};
then x = Top L & Top L <= Top L by TARSKI:def 1;
hence thesis by WAYBEL_0:18;
end;
Lm5:
for L being lower-bounded sup-Semilattice, I being Ideal of L holds
{Bottom L} c= I
proof
let L be lower-bounded sup-Semilattice;
let I be Ideal of L;
let a; assume a in {Bottom L};
then a = Bottom L by TARSKI:def 1;
hence thesis by Th21;
end;
reserve L for lower-bounded sup-Semilattice;
reserve x for Element of L;
theorem Th25:
(the carrier of L) --> {Bottom L} is map of L, InclPoset Ids L
proof
{Bottom L} = downarrow Bottom L by Th23;
then {Bottom L} in {X where X is Ideal of L: not contradiction};
then {Bottom L} in Ids L by WAYBEL_0:def 23;
then {Bottom L} in the carrier of InclPoset Ids L by YELLOW_1:1;
then (the carrier of L) --> {Bottom L} is Function of the carrier of L,
the carrier of InclPoset Ids L by FUNCOP_1:57;
hence thesis ;
end;
Lm6:
for f be map of L, InclPoset Ids L st f = (the carrier of L) --> {Bottom L}
holds f is monotone
proof
let f be map of L, InclPoset Ids L;
assume A1: f = (the carrier of L) --> {Bottom L};
let x,y be Element of L;
f.x = {Bottom L} & f.y = {Bottom L} by A1,FUNCOP_1:13;
hence thesis by YELLOW_1:3;
end;
theorem Th26:
(the carrier of L) --> {Bottom L} in the carrier of MonSet L
proof
set s = (the carrier of L) --> {Bottom L};
ex s' be map of L, InclPoset Ids L st
s = s' & s' is monotone &
for x be Element of L holds s'.x c= downarrow x
proof
reconsider s as map of L, InclPoset Ids L by Th25;
take s;
for x holds s.x c= downarrow x
proof
let x be Element of L;
s.x = {Bottom L} by FUNCOP_1:13;
hence s.x c= downarrow x by Lm5;
end;
hence thesis by Lm6;
end;
hence thesis by Def14;
end;
theorem
for AR being auxiliary Relation of L holds
[(the carrier of L) --> {Bottom L} , AR-below] in the InternalRel of MonSet L
proof
let AR be auxiliary Relation of L;
set c = (the carrier of L) --> {Bottom L}, d = AR-below;
ex f,g be map of L, InclPoset Ids L st c = f & d = g &
c in the carrier of MonSet L & d in the carrier of MonSet L & f <= g
proof
reconsider c as map of L, InclPoset Ids L by Th25;
take c,d;
c <= d
proof
let x be set; assume x in the carrier of L;
then reconsider x' = x as Element of L;
d.x = AR-below x' by Def13;
then reconsider dx = d.x' as Ideal of L;
reconsider dx' = dx as Element of InclPoset Ids L;
c.x' = {Bottom L} by FUNCOP_1:13;
then A1: c.x c= dx by Lm5;
take c.x', dx';
thus thesis by A1,YELLOW_1:3;
end;
hence thesis by Th18,Th26;
end;
hence thesis by Def14;
end;
Lm7:
for L ex x be Element of MonSet L st x is_>=_than the carrier of MonSet L
proof
let L;
set x = IdsMap L;
x in the carrier of MonSet L by Th19;
then reconsider x as Element of MonSet L;
x is_>=_than the carrier of MonSet L
proof
let b be Element of MonSet L;
assume b in the carrier of MonSet L;
consider s be map of L, InclPoset Ids L such that A1: b = s &
s is monotone & for x be Element of L holds s.x c= downarrow x by Def14;
IdsMap L >= s
proof
let a be set; assume a in the carrier of L;
then reconsider a' = a as Element of L;
A2: (IdsMap L).a = downarrow a' by YELLOW_2:def 4;
A3: s.a c= downarrow a' by A1;
reconsider A = s.a',
B = (IdsMap L).a' as Element of InclPoset Ids L;
take A, B;
thus thesis by A2,A3,YELLOW_1:3;
end;
then [b,x] in the InternalRel of MonSet L by A1,Def14;
hence thesis by ORDERS_1:def 9;
end;
hence thesis;
end;
definition let L;
cluster MonSet L -> upper-bounded;
coherence
proof
consider x be Element of MonSet L such that
A1: x is_>=_than the carrier of MonSet L by Lm7;
take x;
thus thesis by A1;
end;
end;
definition let L;
func Rel2Map L -> map of InclPoset Aux L, MonSet L means :Def15:
for AR being auxiliary Relation of L holds it.AR = AR-below;
existence
proof
defpred P[set,set] means
ex AR be auxiliary Relation of L st AR = $1 & $2 = AR-below;
A1: for a st a in the carrier of InclPoset Aux L
ex y be set st y in the carrier of MonSet L & P[a,y]
proof
let a; assume a in the carrier of InclPoset Aux L;
then a in Aux L by YELLOW_1:1;
then reconsider AR = a as auxiliary Relation of L by Def9;
take AR-below;
thus thesis by Th18;
end;
consider f being Function of the carrier of InclPoset Aux L,
the carrier of MonSet L such that
A2: for a st a in the carrier of InclPoset Aux L holds P[a,f.a]
from FuncEx1(A1);
take f;
now let AR be auxiliary Relation of L;
AR in Aux L by Def9;
then AR in the carrier of InclPoset Aux L by YELLOW_1:1;
then P[AR,f.AR] by A2;
hence f.AR = AR-below;
end;
hence thesis ;
end;
uniqueness
proof
let I1, I2 be map of InclPoset Aux L, MonSet L;
assume A3: for AR be auxiliary Relation of L holds I1.AR = AR-below;
assume A4: for AR be auxiliary Relation of L holds I2.AR = AR-below;
dom I1 = the carrier of InclPoset Aux L by FUNCT_2:def 1;
then A5: dom I1 = Aux L by YELLOW_1:1;
dom I2 = the carrier of InclPoset Aux L by FUNCT_2:def 1;
then A6: dom I2 = Aux L by YELLOW_1:1;
now let a; assume a in Aux L;
then reconsider AR = a as auxiliary Relation of L by Def9;
I1.AR = AR-below by A3
.= I2.AR by A4;
hence I1.a = I2.a;
end;
hence thesis by A5,A6,FUNCT_1:9;
end;
end;
theorem
for R1, R2 being auxiliary Relation of L st R1 c= R2 holds
R1-below <= R2-below
proof
let R1, R2 be auxiliary Relation of L; assume A1: R1 c= R2;
let x be set;
assume x in the carrier of L;
then reconsider x' = x as Element of L;
A2: R1-below x' c= R2-below x'
proof
let a; assume a in R1-below x';
then a in {y where y is Element of L: [y,x'] in R1} by Def11;
then consider b be Element of L such that A3: b = a & [b,x'] in R1;
b in {y where y is Element of L: [y,x'] in R2} by A1,A3;
hence thesis by A3,Def11;
end;
reconsider A1 = (R1-below).x', A2 = (R2-below).x'
as Element of InclPoset Ids L;
take A1, A2;
(R1-below).x = R1-below x' &
(R2-below).x = R2-below x' by Def13;
hence thesis by A2,YELLOW_1:3;
end;
theorem Th29:
for R1, R2 being Relation of L st R1 c= R2 holds
R1-below x c= R2-below x
proof
let R1, R2 be Relation of L; assume A1: R1 c= R2;
let a; assume a in R1-below x;
then a in {z where z is Element of L: [z,x] in R1} by Def11;
then consider b be Element of L such that A2: b = a & [b,x] in R1;
b in {z where z is Element of L: [z,x] in R2} by A1,A2;
hence thesis by A2,Def11;
end;
Lm8:
Rel2Map L is monotone
proof
let x,y be Element of InclPoset Aux L;
x in the carrier of InclPoset Aux L &
y in the carrier of InclPoset Aux L;
then x in Aux L & y in Aux L by YELLOW_1:1;
then reconsider R1 = x, R2 = y as auxiliary Relation of L by Def9;
assume x <= y;
then A1: x c= y by YELLOW_1:3;
let a, b be Element of MonSet L;
assume A2: a = (Rel2Map L).x & b = (Rel2Map L).y;
thus a <= b
proof
A3: (Rel2Map L).x = R1-below & (Rel2Map L).y = R2-below by Def15;
consider s be map of L, InclPoset Ids L such that
A4: (Rel2Map L).x = s & s is monotone &
for x be Element of L holds s.x c= downarrow x by Def14;
consider t be map of L, InclPoset Ids L such that
A5: (Rel2Map L).y = t & t is monotone &
for x be Element of L holds t.x c= downarrow x by Def14;
s <= t
proof
let q be set; assume q in the carrier of L;
then reconsider q' = q as Element of L;
A6: s.q = R1-below q' by A3,A4,Def13;
A7: t.q = R2-below q' by A3,A5,Def13;
A8: R1-below q' c= R2-below q' by A1,Th29;
reconsider sq = s.q', tq = t.q' as Element of InclPoset Ids L;
sq <= tq by A6,A7,A8,YELLOW_1:3;
hence thesis;
end;
then [R1-below, R2-below] in the InternalRel of MonSet L
by A3,A4,A5,Def14;
hence thesis by A2,A3,ORDERS_1:def 9;
end;
end;
definition let L;
cluster Rel2Map L -> monotone;
coherence by Lm8;
end;
definition let L;
func Map2Rel L -> map of MonSet L, InclPoset Aux L means :Def16:
for s be set st s in the carrier of MonSet L
ex AR be auxiliary Relation of L st AR = it.s &
for x,y be set holds
[x,y] in AR iff ex x',y' be Element of L,
s' be map of L, InclPoset Ids L st
x' = x & y' = y & s' = s & x' in s'.y';
existence
proof
defpred P[set, set] means
ex AR be auxiliary Relation of L st AR = $2 & for x,y be set holds
[x,y] in AR iff ex x',y' be Element of L,
s' be map of L, InclPoset Ids L st
x' = x & y' = y & s' = $1 & x' in s'.y';
A1: for a st a in the carrier of MonSet L ex b be set st b in the carrier of
InclPoset Aux L & P[a,b]
proof
let a; assume A2: a in the carrier of MonSet L;
defpred Q[set,set] means
ex x', y' be Element of L, s' be map of L, InclPoset Ids L st
x' = $1 & y' = $2 & s' = a & x' in s'.y';
consider R being Relation of the carrier of L, the carrier of L such that
A3: for x,y be set holds [x,y] in R iff
x in the carrier of L & y in the carrier of L & Q[x,y]
from Rel_On_Set_Ex;
reconsider R as Relation of L ;
now
thus R is auxiliary(i)
proof
let x, y be Element of L;
assume [x,y] in R;
then consider x', y' be Element of L,
s' be map of L, InclPoset Ids L such that
A4: x' = x & y' = y & s' = a & x' in s'.y' by A3;
consider s be map of L, InclPoset Ids L
such that A5: a = s & s is monotone &
for x be Element of L holds s.x c= downarrow x by A2,Def14;
s'.y c= downarrow y by A4,A5;
hence x <= y by A4,WAYBEL_0:17;
end;
thus R is auxiliary(ii)
proof
let x, y, z, u be Element of L;
assume A6: u <= x & [x,y] in R & y <= z;
then consider x', y' be Element of L,
s' be map of L, InclPoset Ids L such that
A7: x' = x & y' = y & s' = a & x' in s'.y' by A3;
consider s be map of L, InclPoset Ids L
such that A8: a = s & s is monotone &
for x be Element of L holds s.x c= downarrow x by A2,Def14;
reconsider sy = s.y, sz = s.z as Element of InclPoset Ids L;
sy <= sz by A6,A8,ORDERS_3:def 5;
then A9: s.y c= s.z by YELLOW_1:3;
s.z in the carrier of InclPoset Ids L;
then s.z in Ids L by YELLOW_1:1;
then s.z in {X where X is Ideal of L: not contradiction} by WAYBEL_0:def
23;
then consider sz be Ideal of L such that A10: s.z = sz;
u in sz by A6,A7,A8,A9,A10,WAYBEL_0:def 19;
hence thesis by A3,A8,A10;
end;
thus R is auxiliary(iii)
proof
let x, y, z be Element of L;
assume A11: [x,z] in R & [y,z] in R;
then consider x1, z1 be Element of L,
s1 be map of L, InclPoset Ids L such that
A12: x1 = x & z1 = z & s1 = a & x1 in s1.z1 by A3;
consider y2, z2 be Element of L,
s2 be map of L, InclPoset Ids L such that
A13: y2 = y & z2 = z & s2 = a & y2 in s2.z2 by A3,A11;
s1.z in the carrier of InclPoset Ids L;
then s1.z in Ids L by YELLOW_1:1;
then s1.z in {X where X is Ideal of L: not contradiction} by WAYBEL_0:
def 23;
then consider sz be Ideal of L such that A14: s1.z = sz;
consider z3 be Element of L such that A15: z3 in sz & x <= z3 & y <= z3
by A12,A13,A14,WAYBEL_0:def 1;
ex q being Element of L st x <= q & y <= q &
for c being Element of L st x <= c & y <= c holds q <= c
by LATTICE3:def 10;
then x "\/" y <= z3 by A15,LATTICE3:def 13;
then x "\/" y in sz by A15,WAYBEL_0:def 19;
hence thesis by A3,A12,A14;
end;
thus R is auxiliary(iv)
proof
let x be Element of L;
reconsider x' = Bottom L, y' = x as Element of L;
consider s' be map of L, InclPoset Ids L
such that A16: a = s' & s' is monotone &
for x be Element of L holds s'.x c= downarrow x by A2,Def14;
s'.y' in the carrier of InclPoset Ids L;
then s'.y' in Ids L by YELLOW_1:1;
then s'.y' in {X where X is Ideal of L: not contradiction}
by WAYBEL_0:def 23;
then consider sy be Ideal of L such that A17: sy = s'.y';
x' in sy by Th21;
hence thesis by A3,A16,A17;
end;
end;
then reconsider R as auxiliary Relation of L by Def8;
A18: for x,y be set holds [x,y] in R iff
ex x',y' be Element of L, s' be map of L, InclPoset Ids L st
x' = x & y' = y & s' = a & x' in s'.y' by A3;
take b = R;
b in Aux L by Def9;
hence thesis by A18,YELLOW_1:1;
end;
consider f being Function of the carrier of MonSet L, the carrier of
InclPoset Aux L such that
A19: for a st a in
the carrier of MonSet L holds P[a,f.a] from FuncEx1 (A1);
reconsider f' = f as map of MonSet L, InclPoset Aux L
;
take f';
let s be set; assume A20: s in the carrier of MonSet L;
then reconsider s' = s as Element of MonSet L;
f'.s' in the carrier of InclPoset Aux L;
then f'.s' in Aux L by YELLOW_1:1;
then reconsider fs = f'.s' as auxiliary Relation of L by Def9;
take fs;
ex AR be auxiliary Relation of L st AR = f'.s & for x,y be set holds
[x,y] in AR iff ex x',y' be Element of L,
s' be map of L, InclPoset Ids L st
x' = x & y' = y & s' = s & x' in s'.y' by A19,A20;
hence thesis;
end;
uniqueness
proof
let M1, M2 be map of MonSet L, InclPoset Aux L;
assume A21: for s be set st s in the carrier of MonSet L
ex AR be auxiliary Relation of L st AR = M1.s &
for x,y be set holds
[x,y] in AR iff ex x',y' be Element of L,
s' be map of L, InclPoset Ids L st
x' = x & y' = y & s' = s & x' in s'.y';
assume A22: for s be set st s in the carrier of MonSet L
ex AR be auxiliary Relation of L st AR = M2.s &
for x,y be set holds
[x,y] in AR iff ex x',y' be Element of L,
s' be map of L, InclPoset Ids L st
x' = x & y' = y & s' = s & x' in s'.y';
M1 = M2
proof
A23: dom M1 = the carrier of MonSet L by FUNCT_2:def 1;
A24: dom M2 = the carrier of MonSet L by FUNCT_2:def 1;
for s be set st s in the carrier of MonSet L holds M1.s = M2.s
proof
let s be set; assume A25: s in the carrier of MonSet L;
then consider AR1 be auxiliary Relation of L such that A26: AR1 = M1.s &
for x,y be set holds
[x,y] in AR1 iff ex x',y' be Element of L,
s' be map of L, InclPoset Ids L st
x' = x & y' = y & s' = s & x' in s'.y' by A21;
consider AR2 be auxiliary Relation of L such that A27: AR2 = M2.s &
for x,y be set holds
[x,y] in AR2 iff ex x',y' be Element of L,
s' be map of L, InclPoset Ids L st
x' = x & y' = y & s' = s & x' in s'.y' by A22,A25;
AR1 = AR2
proof
let x,y be set;
hereby assume [x,y] in AR1;
then consider x',y' be Element of L,
s' be map of L, InclPoset Ids L such that
A28: x' = x & y' = y & s' = s & x' in s'.y' by A26;
thus [x,y] in AR2 by A27,A28;
end;
assume [x,y] in AR2;
then consider x',y' be Element of L,
s' be map of L, InclPoset Ids L such that
A29: x' = x & y' = y & s' = s & x' in s'.y' by A27;
thus [x,y] in AR1 by A26,A29;
end;
hence thesis by A26,A27;
end;
hence thesis by A23,A24,FUNCT_1:9;
end;
hence thesis;
end;
end;
Lm9:
Map2Rel L is monotone
proof
set f = Map2Rel L;
A1:InclPoset Aux L = RelStr (#Aux L, RelIncl Aux L#) by YELLOW_1:def 1;
let x,y be Element of MonSet L;
assume x <= y;
then [x,y] in the InternalRel of MonSet L by ORDERS_1:def 9;
then consider s,t be map of L, InclPoset Ids L such that
A2:x = s & y = t & x in the carrier of MonSet L & y in
the carrier of MonSet L &
s <= t by Def14;
A3: f.s in the carrier of InclPoset Aux L &
f.t in the carrier of InclPoset Aux L by A2,FUNCT_2:7;
then A4: f.s in Aux L & f.t in Aux L by YELLOW_1:1;
then reconsider AS = f.s, AT = f.t as auxiliary Relation of L by Def9;
reconsider AS' = AS, AT' = AT as Element of InclPoset Aux L
by A3;
AS' c= AT'
proof
for a,b be set st [a,b] in AS holds [a,b] in AT
proof
let a,b be set; assume A5: [a,b] in AS;
then A6: a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
then reconsider a' = a, b' = b as Element of L;
reconsider sb = s.b', tb = t.b' as Element of InclPoset Ids L;
consider a1, b1 being Element of InclPoset Ids L such that
A7: a1 = s.b & b1 = t.b & a1 <= b1 by A2,A6,YELLOW_2:def 1;
A8: sb c= tb by A7,YELLOW_1:3;
consider AR be auxiliary Relation of L such that A9: AR = f.x &
for a',b' be set holds
[a',b'] in AR iff ex x',y' be Element of L,
s' be map of L, InclPoset Ids L st
x' = a' & y' = b' & s' = x & x' in s'.y' by Def16;
consider x',y' be Element of L,
s' be map of L, InclPoset Ids L such that
A10: x' = a' & y' = b' & s' = s & x' in s'.y' by A2,A5,A9;
consider AR1 be auxiliary Relation of L such that A11: AR1 = f.y &
for a',b' be set holds
[a',b'] in AR1 iff ex x',y' be Element of L,
s' be map of L, InclPoset Ids L st
x' = a' & y' = b' & s' = y & x' in s'.y' by Def16;
thus thesis by A2,A8,A10,A11;
end;
hence thesis by RELAT_1:def 3;
end;
then [AS',AT'] in RelIncl Aux L by A4,WELLORD2:def 1;
hence thesis by A1,A2,ORDERS_1:def 9;
end;
definition let L;
cluster Map2Rel L -> monotone;
coherence by Lm9;
end;
theorem Th30:
(Map2Rel L) * (Rel2Map L) = id dom (Rel2Map L)
proof
set LS = (Map2Rel L) * (Rel2Map L);
set R = id dom (Rel2Map L);
dom LS = the carrier of InclPoset Aux L by FUNCT_2:def 1;
then A1: dom LS = Aux L by YELLOW_1:1;
dom R = dom (Rel2Map L) by FUNCT_1:34;
then dom R = the carrier of InclPoset Aux L by FUNCT_2:def 1;
then A2: dom R = Aux L by YELLOW_1:1;
for a st a in Aux L holds LS.a = R.a
proof
let a; assume A3: a in Aux L;
then reconsider AR = a as auxiliary Relation of L by Def9;
A4: a in the carrier of InclPoset Aux L by A3,YELLOW_1:1;
then A5: a in dom (Rel2Map L) by FUNCT_2:def 1;
then LS.a = (Map2Rel L).((Rel2Map L).AR) by FUNCT_1:23;
then A6: LS.a = (Map2Rel L).(AR-below) by Def15;
LS.a in the carrier of InclPoset Aux L by A4,FUNCT_2:7;
then LS.a in Aux L by YELLOW_1:1;
then reconsider La = LS.a as auxiliary Relation of L by Def9;
A7: AR-below in the carrier of MonSet L by Th18;
La = AR
proof
for c,b be set holds [c,b] in La iff [c,b] in AR
proof
let c,b be set;
hereby assume A8: [c,b] in La;
consider AR' be auxiliary Relation of L such that A9:
AR' = (Map2Rel L).(AR-below) &
for c,b be set holds
[c,b] in AR' iff ex c',b' be Element of L,
s' be map of L, InclPoset Ids L st
c' = c & b' = b & s' = AR-below & c' in s'.b' by A7,Def16;
consider c',b' be Element of L,
s' be map of L, InclPoset Ids L such that
A10: c' = c & b' = b & s' = AR-below & c' in s'.b' by A6,A8,A9;
c' in AR-below b' by A10,Def13;
hence [c,b] in AR by A10,Th13;
end;
assume A11: [c,b] in AR;
then c in the carrier of L & b in the carrier of L by ZFMISC_1:106;
then reconsider c' = c, b' = b as Element of L;
c' in AR-below b' by A11,Th13;
then A12: c' in (AR-below).b' by Def13;
consider AR' be auxiliary Relation of L such that
A13: AR' = (Map2Rel L).(AR-below) &
for c,b be set holds
[c,b] in AR' iff ex c',b' be Element of L,
s' be map of L, InclPoset Ids L st
c' = c & b' = b & s' = AR-below & c' in s'.b' by A7,Def16;
thus [c,b] in La by A6,A12,A13;
end;
hence thesis by RELAT_1:def 2;
end;
hence thesis by A5,FUNCT_1:35;
end;
hence LS = R by A1,A2,FUNCT_1:9;
end;
theorem Th31:
(Rel2Map L) * (Map2Rel L) = id (the carrier of MonSet L)
proof
set LS = (Rel2Map L) * (Map2Rel L);
set R = id (the carrier of MonSet L);
A1: dom LS = the carrier of MonSet L by FUNCT_2:def 1;
A2: dom R = the carrier of MonSet L by FUNCT_1:34;
for a st a in the carrier of MonSet L holds LS.a = R.a
proof
let a; assume A3: a in the carrier of MonSet L;
then consider s be map of L, InclPoset Ids L such that
A4: a = s & s is monotone &
for x be Element of L holds s.x c= downarrow x by Def14;
LS.s in the carrier of MonSet L by A3,A4,FUNCT_2:7;
then consider Ls be map of L, InclPoset Ids L such that
A5: LS.s = Ls & Ls is monotone &
for x be Element of L holds Ls.x c= downarrow x by Def14;
set AR = (Map2Rel L).s;
AR in the carrier of InclPoset Aux L by A3,A4,FUNCT_2:7;
then AR in Aux L by YELLOW_1:1;
then reconsider AR as auxiliary Relation of L by Def9;
dom (Map2Rel L) = the carrier of MonSet L by FUNCT_2:def 1;
then Ls = (Rel2Map L).AR by A3,A4,A5,FUNCT_1:23;
then A6: Ls = AR-below by Def15;
Ls = s
proof
A7: dom Ls = the carrier of L by FUNCT_2:def 1;
A8: dom s = the carrier of L by FUNCT_2:def 1;
now let b be set; assume A9: b in the carrier of L;
then reconsider b' = b as Element of L;
thus Ls.b = s.b
proof
thus Ls.b c= s.b
proof
let d be set; assume d in Ls.b;
then d in AR-below b' by A6,Def13;
then A10: [d,b'] in AR by Th13;
consider AR' be auxiliary Relation of L such that A11:
AR' = (Map2Rel L).s & for d,b' be set holds
[d,b'] in AR' iff ex d',b'' be Element of L,
s' be map of L, InclPoset Ids L st
d' = d & b'' = b' & s' = s & d' in s'.b'' by A3,A4,Def16;
consider d',b'' be Element of L,
s' be map of L, InclPoset Ids L such that
A12: d' = d & b'' = b' & s' = s & d' in s'.b'' by A10,A11;
thus thesis by A12;
end;
thus s.b c= Ls.b
proof
let d be set; assume A13: d in s.b;
s.b in the carrier of InclPoset Ids L by A9,FUNCT_2:7;
then s.b in Ids L by YELLOW_1:1;
then s.b in {X where X is Ideal of L: not contradiction} by WAYBEL_0:
def 23;
then consider X be Ideal of L such that A14: s.b = X;
reconsider d' = d as Element of L by A13,A14;
consider AR' be auxiliary Relation of L such that A15:
AR' = (Map2Rel L).s & for d,b' be set holds
[d,b'] in AR' iff ex d',b'' be Element of L,
s' be map of L, InclPoset Ids L st
d' = d & b'' = b' & s' = s & d' in s'.b'' by A3,A4,Def16;
[d',b'] in AR by A13,A15;
then d' in AR-below b' by Th13;
hence thesis by A6,Def13;
end;
end;
end;
hence thesis by A7,A8,FUNCT_1:9;
end;
hence LS.a = R.a by A3,A4,A5,FUNCT_1:35;
end;
hence thesis by A1,A2,FUNCT_1:9;
end;
definition let L;
cluster Rel2Map L -> one-to-one;
coherence
proof
ex g be Function st g*(Rel2Map L) = id dom (Rel2Map L)
proof
take Map2Rel L;
thus thesis by Th30;
end;
hence Rel2Map L is one-to-one by FUNCT_1:53;
end;
end;
:: Proposition 1.10 (i) p.43
theorem Th32:
(Rel2Map L)" = Map2Rel L
proof
(Rel2Map L)*(Map2Rel L) = id (the carrier of MonSet L) implies
rng (Rel2Map L) = the carrier of MonSet L by FUNCT_2:24;
then Rel2Map L is one-to-one & rng (Rel2Map L) = dom (Map2Rel L) &
(Map2Rel L)*(Rel2Map L) = id dom (Rel2Map L)
by Th30,Th31,FUNCT_2:def 1;
hence Map2Rel L = (Rel2Map L)" by FUNCT_1:63;
end;
:: Proposition 1.10 (ii) p.43
theorem
Rel2Map L is isomorphic
proof
ex g being map of MonSet L, InclPoset Aux L st
g = (Rel2Map L)" & g is monotone
proof
reconsider g = Map2Rel L as map of MonSet L, InclPoset Aux L;
take g;
thus thesis by Th32;
end;
hence thesis by WAYBEL_0:def 38;
end;
theorem Th34:
for L being complete LATTICE, x being Element of L holds
meet { I where I is Ideal of L : x <= sup I } = waybelow x
proof
let L be complete LATTICE, x be Element of L;
set X = { I where I is Ideal of L : x <= sup I };
X c= bool the carrier of L
proof
let a; assume a in X;
then consider I be Ideal of L such that A1: a = I & x <= sup I;
thus thesis by A1;
end;
then reconsider X' = X as Subset-Family of L by SETFAM_1:def 7
;
sup downarrow x = x by WAYBEL_0:34;
then A2:downarrow x in X;
thus meet X c= waybelow x
proof
let a; assume A3: a in meet X;
then a in meet X';
then reconsider y = a as Element of L;
now let I be Ideal of L; assume x <= sup I;
then I in X;
hence y in I by A3,SETFAM_1:def 1;
end;
then y << x by WAYBEL_3:21;
hence thesis by WAYBEL_3:7;
end;
thus waybelow x c= meet X
proof
let a; assume a in waybelow x;
then a in {y where y is Element of L: y << x} by WAYBEL_3:def 3;
then consider a' be Element of L such that A4: a' = a & a' << x;
for Y be set holds Y in X implies a in Y
proof
let Y be set; assume Y in X;
then consider I be Ideal of L such that A5: Y = I & x <= sup I;
thus thesis by A4,A5,WAYBEL_3:20;
end;
hence thesis by A2,SETFAM_1:def 1;
end;
end;
scheme LambdaC'{ A() -> non empty RelStr, C[set], F(set) -> set,
G(set) -> set } :
ex f being Function st dom f = the carrier of A() &
for x be Element of A() holds
(C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x))
proof
defpred c[set] means C[$1];
deffunc f(set) = F($1);
deffunc g(set) = G($1);
A1: ex f being Function st dom f = the carrier of A() &
for x be set st x in the carrier of A() holds
(c[x] implies f.x = f(x)) & (not c[x] implies f.x = g(x)) from LambdaC;
thus ex f being Function st dom f = the carrier of A() &
for x be Element of A() holds
(C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x))
proof
consider f being Function such that A2: dom f = the carrier of A() &
for x be set st x in the carrier of A() holds
(C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)) by A1;
take f;
thus dom f = the carrier of A() by A2;
let x be Element of A();
thus (C[x] implies f.x = F(x)) & (not C[x] implies f.x = G(x)) by A2;
end;
end;
definition let L be Semilattice, I be Ideal of L;
func DownMap I -> map of L, InclPoset Ids L means :Def17:
for x be Element of L holds
( x <= sup I implies it.x = ( downarrow x ) /\ I ) &
( not x <= sup I implies it.x = downarrow x );
existence
proof
defpred P[set,set] means
for x be Element of L st x = $1 holds
( x <= sup I implies $2 = ( downarrow x ) /\ I ) &
( not x <= sup I implies $2 = downarrow x );
defpred C[Element of L] means $1 <= sup I;
deffunc F(Element of L) = ( downarrow $1 ) /\ I;
deffunc G(Element of L) = downarrow $1;
consider f being Function such that
A1: dom f = the carrier of L &
for x be Element of L holds
( C[x] implies f.x = F(x) ) &
( not C[x] implies f.x = G(x) ) from LambdaC';
A2: for a be set st a in the carrier of L ex y be set st y in
the carrier of InclPoset Ids L & P[a,y]
proof let a; assume a in the carrier of L;
then reconsider x = a as Element of L;
take y = f.x;
thus y in the carrier of InclPoset Ids L
proof
per cases;
suppose x <= sup I;
then y = ( downarrow x ) /\ I by A1;
then y is Ideal of L by YELLOW_2:42;
then y in {X where X is Ideal of L: not contradiction};
then y in Ids L by WAYBEL_0:def 23;
hence thesis by YELLOW_1:1;
suppose not x <= sup I;
then y = downarrow x by A1;
then y in {X where X is Ideal of L: not contradiction};
then y in Ids L by WAYBEL_0:def 23;
hence thesis by YELLOW_1:1;
end;
thus P[a,y] by A1;
end;
consider f being Function of the carrier of L,
the carrier of InclPoset Ids L such that
A3: for a st a in the carrier of L holds P[a,f.a] from FuncEx1(A2);
reconsider f as map of L, InclPoset Ids L ;
for x be Element of L holds
( x <= sup I implies f.x = ( downarrow x ) /\ I ) &
( not x <= sup I implies f.x = downarrow x ) by A3;
hence thesis;
end;
uniqueness
proof
let M1, M2 be map of L, InclPoset Ids L;
assume A4: for x be Element of L holds
( x <= sup I implies M1.x = ( downarrow x ) /\ I ) &
( not x <= sup I implies M1.x = downarrow x );
assume A5: for x be Element of L holds
( x <= sup I implies M2.x = ( downarrow x ) /\ I ) &
( not x <= sup I implies M2.x = downarrow x );
A6: dom M1 = the carrier of L by FUNCT_2:def 1;
A7: dom M2 = the carrier of L by FUNCT_2:def 1;
now let x be set; assume x in the carrier of L;
then reconsider x' = x as Element of L;
A8: now assume A9: x' <= sup I;
then M1.x' = ( downarrow x' ) /\ I by A4;
hence M1.x' = M2.x' by A5,A9;
end;
now assume A10: not x' <= sup I;
then M1.x' = downarrow x' by A4;
hence M1.x' = M2.x' by A5,A10;
end;
hence M1.x = M2.x by A8;
end;
hence thesis by A6,A7,FUNCT_1:9;
end;
end;
Lm10:
for L be Semilattice, I be Ideal of L holds
DownMap I is monotone
proof
let L be Semilattice, I be Ideal of L;
let x,y be Element of L;
assume A1: x <= y;
per cases;
suppose x <= sup I & y <= sup I;
then A2: (DownMap I).x = (downarrow x) /\ I & (DownMap I).y = (downarrow y) /\
I by Def17;
downarrow x c= downarrow y by A1,WAYBEL_0:21;
then (DownMap I).x c= (DownMap I).y by A2,XBOOLE_1:26;
hence thesis by YELLOW_1:3;
suppose x <= sup I & not y <= sup I;
then A3: (DownMap I).x = (downarrow x) /\ I & (DownMap I).y = downarrow y by
Def17;
A4:downarrow x c= downarrow y by A1,WAYBEL_0:21;
(downarrow x) /\ I c= downarrow x by XBOOLE_1:17;
then (DownMap I).x c= (DownMap I).y by A3,A4,XBOOLE_1:1;
hence thesis by YELLOW_1:3;
suppose not x <= sup I & y <= sup I;
hence thesis by A1,ORDERS_1:26;
suppose not x <= sup I & not y <= sup I;
then (DownMap I).x = downarrow x & (DownMap I).y = downarrow y by Def17;
then (DownMap I).x c= (DownMap I).y by A1,WAYBEL_0:21;
hence thesis by YELLOW_1:3;
end;
Lm11:
for L be Semilattice, x be Element of L
for I be Ideal of L holds (DownMap I).x c= downarrow x
proof
let L be Semilattice, x be Element of L;
let I be Ideal of L;
per cases;
suppose x <= sup I;
then (DownMap I).x = (downarrow x) /\ I by Def17;
hence thesis by XBOOLE_1:17;
suppose not x <= sup I;
hence thesis by Def17;
end;
theorem Th35:
for L being Semilattice, I being Ideal of L holds
DownMap I in the carrier of MonSet L
proof
let L be Semilattice, I be Ideal of L;
reconsider mI = DownMap I as map of L, InclPoset Ids L;
ex s be map of L, InclPoset Ids L st mI = s &
s is monotone &
for x be Element of L holds s.x c= downarrow x
proof
take mI;
thus thesis by Lm10,Lm11;
end;
hence thesis by Def14;
end;
theorem Th36:
for L being with_infima antisymmetric reflexive RelStr, x being Element of L
for D being non empty lower Subset of L holds
{x} "/\" D = (downarrow x) /\ D
proof
let L be with_infima antisymmetric reflexive RelStr, x be Element of L;
let D be non empty lower Subset of L;
A1: {x} "/\" D = { x' "/\" y where x', y is Element of L : x' in {x} & y in D }
by YELLOW_4:def 4;
thus {x} "/\" D c= (downarrow x) /\ D
proof
let a; assume a in {x} "/\" D;
then a in { x' "/\" y where x', y is Element of L : x' in {x} & y in D }
by YELLOW_4:def 4;
then consider x', y be Element of L such that
A2: a = x' "/\" y & x' in {x} & y in D;
reconsider a' = a as Element of L by A2;
A3: x' = x by A2,TARSKI:def 1;
ex v being Element of L st x' >= v & y >= v &
for c being Element of L st x' >= c & y >= c holds v >= c
by LATTICE3:def 11;
then A4: x' "/\" y <= x' & x' "/\" y <= y by LATTICE3:def 14;
then A5: a in downarrow x by A2,A3,WAYBEL_0:17;
a' in D by A2,A4,WAYBEL_0:def 19;
hence a in (downarrow x) /\ D by A5,XBOOLE_0:def 3;
end;
thus (downarrow x) /\ D c= {x} "/\" D
proof
let a; assume A6: a in (downarrow x) /\ D;
then A7: a in downarrow x & a in D by XBOOLE_0:def 3;
reconsider a' = a as Element of D by A6,XBOOLE_0:def 3;
A8: x in {x} by TARSKI:def 1;
a' <= x by A7,WAYBEL_0:17;
then a' = a' "/\" x by YELLOW_0:25;
hence a in {x} "/\" D by A1,A8;
end;
end;
begin :: Approximating Relations
:: Definition 1.11 p.44
definition let L be non empty RelStr, AR be Relation of L;
attr AR is approximating means :Def18:
for x be Element of L holds x = sup (AR-below x);
end;
definition let L be non empty Poset; let mp be map of L, InclPoset Ids L;
attr mp is approximating means :Def19:
for x be Element of L
ex ii be Subset of L st ii = mp.x & x = sup ii;
end;
:: Lemma 1.12 (i) p.44
theorem Th37:
for L being lower-bounded meet-continuous Semilattice, I being Ideal of L
holds DownMap I is approximating
proof
let L be lower-bounded meet-continuous Semilattice;
let I be Ideal of L;
for x be Element of L ex ii be Subset of L st
ii = (DownMap I).x & x = sup ii
proof
let x be Element of L;
set ii = (DownMap I).x;
ii in the carrier of InclPoset Ids L;
then ii in Ids L by YELLOW_1:1;
then ii in {X where X is Ideal of L: not contradiction} by WAYBEL_0:def 23
;
then consider ii' be Ideal of L such that A1: ii' = ii;
reconsider dI = ( downarrow x ) /\ I as Subset of L;
per cases;
suppose A2: x <= sup I;
then sup ii' = sup dI by A1,Def17
.= sup ({x} "/\" I) by Th36
.= x "/\" sup I by WAYBEL_2:def 6
.= x by A2,YELLOW_0:25;
hence thesis by A1;
suppose not x <= sup I;
then sup ii' = sup downarrow x by A1,Def17
.= x by WAYBEL_0:34;
hence thesis by A1;
end;
hence thesis by Def19;
end;
Lm12:
for L be complete LATTICE, x be Element of L
for D be directed Subset of L holds sup ({x} "/\" D) <= x
proof
let L be complete LATTICE, x be Element of L;
let D be directed Subset of L;
A1: {x} "/\" D = { a "/\" b where a, b is Element of L : a in {x} & b in D }
by YELLOW_4:def 4;
A2: ex_sup_of ({x} "/\" D),L by YELLOW_0:17;
for c being Element of L st c in ({x} "/\" D) holds c <= x
proof
let c be Element of L; assume c in ({x} "/\" D);
then consider a, b be Element of L such that
A3: c = a "/\" b & a in {x} & b in D by A1;
a = x by A3,TARSKI:def 1;
hence c <= x by A3,YELLOW_0:23;
end;
then x is_>=_than ({x} "/\" D) by LATTICE3:def 9;
hence sup ({x} "/\" D) <= x by A2,YELLOW_0:30;
end;
:: Lemma 1.12 (ii) p.44
theorem Th38:
for L being lower-bounded continuous LATTICE holds L is meet-continuous
proof
let L be lower-bounded continuous LATTICE;
now let D be non empty directed Subset of L;
let x be Element of L; assume A1: x <= sup D;
A2: ex_sup_of waybelow x,L & ex_sup_of downarrow (sup ({x} "/\" D)),L
by YELLOW_0:17;
waybelow x c= downarrow (sup ({x} "/\" D))
proof
let q be set; assume q in waybelow x;
then q in {y where y is Element of L: y << x} by WAYBEL_3:def 3;
then consider q' be Element of L such that A3: q' = q & q' << x;
A4: q' <= x by A3,WAYBEL_3:1;
consider d be Element of L such that
A5: d in D & q' <= d by A1,A3,WAYBEL_3:def 1;
x in {x} by TARSKI:def 1;
then x "/\" d in { a "/\" b where a, b is Element of L : a in {x} & b in
D } by A5;
then A6: x "/\" d in {x} "/\" D by YELLOW_4:def 4;
ex_inf_of {x,d},L by YELLOW_0:17;
then A7: q' <= x "/\" d by A4,A5,YELLOW_0:19;
sup ({x} "/\" D) is_>=_than {x} "/\" D by YELLOW_0:32;
then x "/\" d <= sup ({x} "/\" D) by A6,LATTICE3:def 9;
then q' <= sup ({x} "/\" D) by A7,ORDERS_1:26;
hence thesis by A3,WAYBEL_0:17;
end;
then sup waybelow x <= sup downarrow (sup ({x} "/\" D)) by A2,YELLOW_0:34;
then sup waybelow x <= sup ({x} "/\" D) by WAYBEL_0:34;
then A8: x <= sup ({x} "/\" D) by WAYBEL_3:def 5;
sup ({x} "/\" D) <= x by Lm12;
hence x = sup ({x} "/\" D) by A8,ORDERS_1:25;
end;
then for x being Element of L, D being non empty directed Subset of L
st x <= sup D holds x = sup ({x} "/\" D);
hence thesis by WAYBEL_2:52;
end;
definition
cluster continuous -> meet-continuous (lower-bounded LATTICE);
coherence by Th38;
end;
:: Lemma 1.12 (iii) p.44
theorem
for L being lower-bounded continuous LATTICE,
I being Ideal of L holds DownMap I is approximating by Th37;
definition let L be non empty reflexive antisymmetric RelStr;
cluster L-waybelow -> auxiliary(i);
coherence
proof
let x, y be Element of L;
assume [x,y] in L-waybelow;
then x << y by Def2;
hence thesis by WAYBEL_3:1;
end;
end;
definition let L be non empty reflexive transitive RelStr;
cluster L-waybelow -> auxiliary(ii);
coherence
proof
set AR = L-waybelow;
let x, y, z, u be Element of L;
assume u <= x & [x,y] in AR & y <= z;
then u <= x & x << y & y <= z by Def2;
then u << z by WAYBEL_3:2;
hence [u,z] in AR by Def2;
end;
end;
definition let L be with_suprema Poset;
cluster L-waybelow -> auxiliary(iii);
coherence
proof
set AR = L-waybelow;
let x, y, z be Element of L;
assume [x,z] in AR & [y,z] in AR;
then x << z & y << z by Def2;
then (x "\/" y) << z by WAYBEL_3:3;
hence [(x "\/" y),z] in AR by Def2;
end;
end;
definition let L be /\-complete (non empty Poset);
cluster L-waybelow -> auxiliary(iii);
coherence
proof
set AR = L-waybelow;
let x, y, z be Element of L;
assume [x,z] in AR & [y,z] in AR;
then x << z & y << z by Def2;
then (x "\/" y) << z by WAYBEL_3:3;
hence [(x "\/" y),z] in AR by Def2;
end;
end;
definition let L be lower-bounded antisymmetric reflexive non empty RelStr;
cluster L-waybelow -> auxiliary(iv);
coherence
proof
let x be Element of L;
Bottom L << x by WAYBEL_3:4;
hence thesis by Def2;
end;
end;
theorem Th40:
for L being complete LATTICE, x being Element of L holds
(L-waybelow)-below x = waybelow x
proof
let L be complete LATTICE, x be Element of L;
set AR = L-waybelow;
A1: AR-below x = {y where y is Element of L: [y,x] in AR} by Def11;
set A = {y where y is Element of L: [y,x] in AR};
set B = {y where y is Element of L: y << x};
A = B
proof
thus A c= B
proof
let a be set;
assume a in A;
then consider v being Element of L such that
A2: a = v and
A3: [v,x] in AR;
v << x by A3,Def2;
hence a in { u' where u' is Element of L : u' << x } by A2;
end;
thus B c= A
proof
let a be set;
assume a in B;
then consider v being Element of L such that
A4: a = v and
A5: v << x;
[v,x] in AR by A5,Def2;
hence a in { u' where u' is Element of L : [u',x] in AR } by A4;
end;
end;
hence thesis by A1,WAYBEL_3:def 3;
end;
theorem Th41:
for L being LATTICE holds IntRel L is approximating
proof
let L be LATTICE;
set AR = IntRel L;
let x be Element of L;
set A = {y where y is Element of L: [y,x] in AR};
set E = { u where u is Element of L : u <= x };
A1: {y where y is Element of L: [y,x] in AR} = E
proof
thus A c= E
proof
let a be set; assume a in A;
then consider v being Element of L such that
A2: a = v and
A3: [v,x] in AR;
v <= x by A3,Lm1;
hence a in E by A2;
end;
thus E c= A
proof
let a be set; assume a in E;
then consider v being Element of L such that
A4: a = v and
A5: v <= x;
[v,x] in AR by A5,Lm1;
hence a in A by A4;
end;
end;
{y where y is Element of L: y <= x } c= the carrier of L
proof let z be set; assume z in {y where y is Element of L: y <= x };
then ex y being Element of L st z = y & y <= x;
hence thesis;
end;
then reconsider E as Subset of L;
A6: x is_>=_than E
proof
let b be Element of L; assume b in E;
then consider b' be Element of L such that A7: b' = b & b' <= x;
thus b <= x by A7;
end;
now
let b be Element of L; assume A8: b is_>=_than E;
x in E;
hence x <= b by A8,LATTICE3:def 9;
end;
then sup E = x by A6,YELLOW_0:30;
hence thesis by A1,Def11;
end;
Lm13:
for L be lower-bounded continuous LATTICE holds
L-waybelow is approximating
proof
let L be lower-bounded continuous LATTICE;
let x be Element of L;
x = sup waybelow x by WAYBEL_3:def 5;
hence thesis by Th40;
end;
definition let L be lower-bounded continuous LATTICE;
cluster L-waybelow -> approximating;
coherence by Lm13;
end;
definition let L be complete LATTICE;
cluster approximating auxiliary Relation of L;
existence
proof
reconsider A = IntRel L as auxiliary Relation of L;
A is approximating by Th41;
hence thesis;
end;
end;
definition let L be complete LATTICE;
defpred P[set] means
$1 is approximating auxiliary Relation of L;
func App L means :Def20:
a in it iff a is approximating auxiliary Relation of L;
existence
proof
consider X be set such that
A1: for a holds a in X iff a in Aux L & P[a] from Separation;
take X;
a is approximating auxiliary Relation of L implies a in X
proof
assume A2: a is approximating auxiliary Relation of L;
then a in Aux L by Def9;
hence thesis by A1,A2;
end;
hence thesis by A1;
end;
uniqueness
proof
thus for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
end;
end;
definition let L be complete LATTICE;
cluster App L -> non empty;
coherence
proof
consider a be approximating auxiliary Relation of L;
a in App L by Def20;
hence thesis;
end;
end;
theorem Th42:
for L being complete LATTICE
for mp being map of L, InclPoset Ids L st
mp is approximating & mp in the carrier of MonSet L
ex AR being approximating auxiliary Relation of L st AR = (Map2Rel L).mp
proof
let L be complete LATTICE;
let mp be map of L, InclPoset Ids L;
assume A1: mp is approximating & mp in the carrier of MonSet L;
then consider AR be auxiliary Relation of L such that A2: AR = (Map2Rel L).mp
&
for x,y be set holds [x,y] in AR iff ex x',y' be Element of L,
s' be map of L, InclPoset Ids L st
x' = x & y' = y & s' = mp & x' in s'.y' by Def16;
now let x be Element of L;
consider ii be Subset of L such that A3: ii = mp.x & x = sup ii by A1,Def19;
AR-below x = mp.x
proof
thus AR-below x c= mp.x
proof
let a; assume a in AR-below x;
then [a,x] in AR by Th13;
then consider x',y' be Element of L,
s' be map of L, InclPoset Ids L such that
A4: x' = a & y' = x & s' = mp & x' in s'.y' by A2;
thus thesis by A4;
end;
thus mp.x c= AR-below x
proof
let a; assume A5: a in mp.x;
then reconsider a' = a as Element of L by A3;
[a',x] in AR by A2,A5;
hence thesis by Th13;
end;
end;
hence x = sup (AR-below x) by A3;
end;
then reconsider AR as approximating auxiliary Relation of L by Def18;
take AR;
thus thesis by A2;
end;
theorem Th43:
for L being complete LATTICE, x being Element of L holds
meet { (DownMap I).x where I is Ideal of L : not contradiction} = waybelow x
proof
let L be complete LATTICE, x be Element of L;
set A = { (DownMap I).x where I is Ideal of L : not contradiction};
set A1 = { (DownMap I).x where I is Ideal of L : x <= sup I};
A1: A1 = { (downarrow x) /\ I where I is Ideal of L : x <= sup I}
proof
thus A1 c= { (downarrow x) /\ I where I is Ideal of L : x <= sup I}
proof
let a; assume a in A1;
then consider I1 be Ideal of L such that A2: a = (DownMap I1).x & x <= sup
I1;
a = (downarrow x) /\ I1 by A2,Def17;
hence a in { (downarrow x) /\ I where I is Ideal of L : x <= sup I} by A2
;
end;
thus { (downarrow x) /\ I where I is Ideal of L : x <= sup I} c= A1
proof
let a;
assume a in { (downarrow x) /\ I where I is Ideal of L : x <= sup I};
then consider I1 be Ideal of L such that
A3: a = (downarrow x) /\ I1 & x <= sup I1;
a = (DownMap I1).x by A3,Def17;
hence a in A1 by A3;
end;
end;
set A2 = { (DownMap I).x where I is Ideal of L : not x <= sup I};
A4: A2 = { downarrow x where I is Ideal of L : not x <= sup I}
proof
thus A2 c= { downarrow x where I is Ideal of L : not x <= sup I}
proof
let a; assume a in A2;
then consider I1 be Ideal of L such that A5: a = (DownMap I1).x &
not x <= sup I1;
a = (downarrow x) by A5,Def17;
hence a in { (downarrow x) where I is Ideal of L : not x <= sup I} by A5;
end;
thus { (downarrow x) where I is Ideal of L : not x <= sup I} c= A2
proof
let a;
assume a in { (downarrow x) where I is Ideal of L : not x <= sup I};
then consider I1 be Ideal of L such that
A6: a = (downarrow x) & not x <= sup I1;
a = (DownMap I1).x by A6,Def17;
hence a in A2 by A6;
end;
end;
A7: A = A1 \/ A2
proof
thus A c= A1 \/ A2
proof
let a; assume a in A;
then consider I2 be Ideal of L such that A8: a = (DownMap I2).x;
x <= sup I2 or not x <= sup I2;
then a in A1 or a in A2 by A8;
hence thesis by XBOOLE_0:def 2;
end;
thus A1 \/ A2 c= A
proof
let a; assume a in A1 \/ A2;
then a in A1 or a in A2 by XBOOLE_0:def 2;
then consider I2,I3 be Ideal of L such that
A9: ( a = (DownMap I2).x & x <= sup I2)
or ( a = (DownMap I3).x & not x <= sup I3);
per cases by A9;
suppose ( a = (DownMap I2).x & x <= sup I2 );
hence thesis;
suppose ( a = (DownMap I3).x & not x <= sup I3);
hence thesis;
end;
end;
per cases;
suppose A10: x = Bottom L;
A11: A2 = {}
proof
assume A2 <> {};
then reconsider A2' = A2 as non empty set;
consider a be Element of A2';
a in A2';
then consider I1 be Ideal of L such that
A12: a = downarrow x & not x <= sup I1 by A4;
thus contradiction by A10,A12,YELLOW_0:44;
end;
set Dx = downarrow x;
x <= sup Dx by A10,YELLOW_0:44;
then A13: Dx /\ Dx in A1 by A1;
A1 c= { K where K is Ideal of L : x <= sup K}
proof
let a; assume a in A1;
then consider H be Ideal of L such that
A14: a = (downarrow x) /\ H & x <= sup H by A1;
reconsider a' = a as Ideal of L by A14,YELLOW_2:42;
x <= sup a' by A10,YELLOW_0:44;
hence thesis;
end;
then A15: meet { K where K is Ideal of L : x <= sup K} c= meet A1 by A13,
SETFAM_1:7;
A16: meet A1 = {x}
proof
reconsider I' = downarrow x as Ideal of L;
x <= sup I' by A10,YELLOW_0:44;
then (downarrow x) /\ I' in A1 by A1;
then {x} in A1 by A10,Th23;
hence meet A1 c= {x} by SETFAM_1:4;
for Z1 be set st Z1 in A1 holds {x} c= Z1
proof
let Z1 be set; assume Z1 in A1;
then consider Z1' be Ideal of L such that
A17: Z1 = (downarrow x) /\ Z1' & x <= sup Z1' by A1;
A18: {x} c= Z1' by A10,Lm5;
{x} c= downarrow x by A10,Th23;
hence thesis by A17,A18,XBOOLE_1:19;
end;
hence {x} c= meet A1 by A13,SETFAM_1:6;
end;
consider E be Ideal of L;
x <= sup E by A10,YELLOW_0:44;
then A19: E in { K where K is Ideal of L : x <= sup K};
for Z1 be set st Z1 in { K where K is Ideal of L : x <= sup K}
holds meet A1 c= Z1
proof
let Z1 be set; assume Z1 in { K where K is Ideal of L : x <= sup K};
then consider K1 be Ideal of L such that A20: K1 = Z1 & x <= sup K1;
thus thesis by A10,A16,A20,Lm5;
end;
then meet A1 c= meet { K where K is Ideal of L : x <= sup K} by A19,SETFAM_1
:6;
then meet A1 = meet { K where K is Ideal of L : x <= sup K} by A15,XBOOLE_0:
def 10;
hence thesis by A7,A11,Th34;
suppose A21: Bottom L <> x;
set O = downarrow Bottom L;
A22: sup O = Bottom L by WAYBEL_0:34;
then sup O <= x by YELLOW_0:44;
then not x < sup O by ORDERS_1:30;
then not x <= sup O by A21,A22,ORDERS_1:def 10;
then A23: downarrow x in A2 by A4;
reconsider O1 = downarrow x as Ideal of L;
A24: x <= sup O1 by WAYBEL_0:34;
downarrow x = downarrow x /\ O1;
then A25: downarrow x in A1 & downarrow x in { downarrow x where I is Ideal of
L :
x <= sup I } by A1,A24;
A26: meet A2 = downarrow x
proof
thus meet A2 c= downarrow x by A23,SETFAM_1:4;
now let Z1 be set; assume Z1 in A2;
then consider L1 be Ideal of L such that A27: Z1 = downarrow x &
not x <= sup L1 by A4;
thus downarrow x c= Z1 by A27;
end;
hence downarrow x c= meet A2 by A23,SETFAM_1:6;
end;
A28: meet A = (meet A1) /\ (meet A2) by A7,A23,A25,SETFAM_1:10;
A29: meet A1 c= downarrow x by A25,SETFAM_1:4;
then A30: meet A = meet A1 by A26,A28,XBOOLE_1:28;
A31: meet A1 c= (downarrow x) /\
meet { I where I is Ideal of L : x <= sup I}
proof
let a; assume A32: a in meet A1;
thus a in (downarrow x) /\
meet { I where I is Ideal of L : x <= sup I}
proof
reconsider L' = [#]L as Subset of L;
x in the carrier of L;
then A33: x in L' by PRE_TOPC:12;
ex_sup_of L',L by YELLOW_0:17;
then L' is_<=_than sup L' by YELLOW_0:def 9;
then x <= sup L' by A33,LATTICE3:def 9;
then A34: L' in { I where I is Ideal of L : x <= sup I};
a in meet { I where I is Ideal of L : x <= sup I}
proof
now let Y1 be set;
assume Y1 in { I where I is Ideal of L : x <= sup I};
then consider Y1' be Ideal of L such that
A35: Y1 = Y1' & x <= sup Y1';
A36: (downarrow x) /\ Y1' c= Y1' by XBOOLE_1:17;
(downarrow x) /\ Y1' in A1 by A1,A35;
then a in (downarrow x) /\ Y1' by A32,SETFAM_1:def 1;
hence a in Y1 by A35,A36;
end;
hence thesis by A34,SETFAM_1:def 1;
end;
hence thesis by A29,A32,XBOOLE_0:def 3;
end;
end;
(downarrow x) /\ meet { I where I is Ideal of L : x <= sup I} c= meet A1
proof
let a; assume a in (downarrow x) /\
meet { I where I is Ideal of L : x <= sup I};
then A37: a in downarrow x &
a in meet { I where I is Ideal of L : x <= sup I} by XBOOLE_0:def 3;
thus a in meet A1
proof
now let Y1 be set; assume Y1 in { (downarrow x) /\ I
where I is Ideal of L : x <= sup I};
then consider I1 be Ideal of L such that
A38: Y1 = (downarrow x) /\ I1 & x <= sup I1;
I1 in { I where I is Ideal of L : x <= sup I} by A38;
then a in I1 by A37,SETFAM_1:def 1;
hence a in Y1 by A37,A38,XBOOLE_0:def 3;
end;
hence thesis by A1,A25,SETFAM_1:def 1;
end;
end;
then (downarrow x) /\ meet { I where I is Ideal of L : x <= sup I} = meet
A1
by A31,XBOOLE_0:def 10;
then A39: (downarrow x) /\ waybelow x = meet A1 by Th34;
waybelow x c= downarrow x by WAYBEL_3:11;
hence thesis by A30,A39,XBOOLE_1:28;
end;
:: Proposition 1.13 p.45
theorem Th44:
for L being lower-bounded meet-continuous LATTICE, x being Element of L holds
meet {AR-below x where AR is auxiliary Relation of L : AR in App L}
= waybelow x
proof
let L be lower-bounded meet-continuous LATTICE, x be Element of L;
set A = {AR-below x where AR is auxiliary Relation of L
: AR in App L};
consider AA be approximating auxiliary Relation of L;
AA in App L by Def20;
then A1:AA-below x in A;
A2: meet { I where I is Ideal of L : x <= sup I } = waybelow x by Th34;
A3: meet { (DownMap I).x where I is Ideal of L : not contradiction } =
waybelow x by Th43;
consider I1 be Ideal of L;
A4: (DownMap I1).x in { (DownMap I).x where I is Ideal of L :
not contradiction };
{ (DownMap I).x where I is Ideal of L : not contradiction } c= A
proof
let a be set;
assume a in { (DownMap I).x where I is Ideal of L : not contradiction };
then consider I be Ideal of L such that A5: a = (DownMap I).x;
A6: DownMap I is approximating by Th37;
A7: DownMap I in the carrier of MonSet L by Th35;
then consider AR be auxiliary Relation of L such that
A8: AR = (Map2Rel L).(DownMap I) &
for x,y be set holds [x,y] in AR iff ex x',y' be Element of L,
s' be map of L, InclPoset Ids L st
x' = x & y' = y & s' = DownMap I & x' in s'.y' by Def16;
consider AR1 be approximating auxiliary Relation of L such that
A9: AR1 = (Map2Rel L).(DownMap I) by A6,A7,Th42;
consider ii be Subset of L such that
A10: ii = (DownMap I).x & x = sup ii by A6,Def19;
A11: AR-below x = (DownMap I).x
proof
thus AR-below x c= (DownMap I).x
proof
let a; assume a in AR-below x;
then [a,x] in AR by Th13;
then consider x',y' be Element of L,
s' be map of L, InclPoset Ids L such that
A12: x' = a & y' = x & s' = DownMap I & x' in s'.y' by A8;
thus thesis by A12;
end;
thus (DownMap I).x c= AR-below x
proof
let a; assume A13: a in (DownMap I).x;
then reconsider a' = a as Element of L by A10;
[a',x] in AR by A8,A13;
hence thesis by Th13;
end;
end;
AR in App L by A8,A9,Def20;
hence a in A by A5,A11;
end;
hence meet A c= waybelow x by A3,A4,SETFAM_1:7;
thus waybelow x c= meet A
proof
A c= { I where I is Ideal of L : x <= sup I }
proof
let a; assume a in A;
then consider AR be auxiliary Relation of L such that
A14: a = AR-below x & AR in App L;
reconsider AR as approximating auxiliary Relation of L by A14,Def20;
sup (AR-below x) = x by Def18;
hence a in { I where I is Ideal of L : x <= sup I } by A14;
end;
hence thesis by A1,A2,SETFAM_1:7;
end;
end;
reserve L for complete LATTICE;
:: Proposition 1.14 p.45 ( 1 <=> 2 )
theorem Th45:
L is continuous iff
(for R being approximating auxiliary Relation of L holds
L-waybelow c= R & L-waybelow is approximating)
proof
set AR = L-waybelow;
hereby assume A1: L is continuous;
then reconsider L' = L as lower-bounded meet-continuous LATTICE by Th38;
thus for R be approximating auxiliary Relation of L holds AR c= R
& AR is approximating
proof
let R be approximating auxiliary Relation of L;
reconsider R' = R as approximating auxiliary Relation of L';
for a,b be set st [a,b] in AR holds [a,b] in R
proof
let a,b be set; assume A2: [a,b] in AR;
then a in the carrier of L & b in the carrier of L by ZFMISC_1:106;
then reconsider a' = a, b' = b as Element of L';
a' << b' by A2,Def2;
then A3: a' in waybelow b' by WAYBEL_3:7;
A4: meet { A1-below b' where A1 is auxiliary Relation of L' :
A1 in App L' } = waybelow b' by Th44;
R' in App L' by Def20;
then R'-below b' in
{ A1-below b' where A1 is auxiliary Relation of L' :
A1 in App L' };
then waybelow b' c= R'-below b' by A4,SETFAM_1:4;
hence thesis by A3,Th13;
end;
hence AR c= R by RELAT_1:def 3;
thus AR is approximating by A1,Lm13;
end;
end;
assume A5: for R be approximating auxiliary Relation of L holds AR c= R
& AR is approximating;
for x being Element of L holds x = sup waybelow x
proof
let x be Element of L;
x = sup (AR-below x) by A5,Def18;
hence x = sup waybelow x by Th40;
end;
then A6:L is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
for x being Element of L holds waybelow x is non empty directed;
hence L is continuous by A6,WAYBEL_3:def 6;
end;
:: Proposition 1.14 p.45 ( 1 <=> 3 )
theorem
L is continuous iff
(L is meet-continuous &
ex R being approximating auxiliary Relation of L st
for R' being approximating auxiliary Relation of L holds R c= R')
proof
hereby assume A1: L is continuous;
hence L is meet-continuous by Th38;
reconsider R = L-waybelow as approximating auxiliary Relation of L
by A1,Lm13;
take R;
thus for R' be approximating auxiliary Relation of L holds R c= R'
by A1,Th45;
end;
assume A2: L is meet-continuous;
given R be approximating auxiliary Relation of L such that
A3: for R' be approximating auxiliary Relation of L holds R c= R';
for x being Element of L holds x = sup waybelow x
proof
let x be Element of L;
set K = {AR-below x where AR is auxiliary Relation of L :
AR in App L};
A4: meet K = waybelow x by A2,Th44;
R in App L by Def20;
then A5: R-below x in K;
then A6: waybelow x c= R-below x by A4,SETFAM_1:4;
A7: sup (R-below x) = x by Def18;
for a st a in K holds R-below x c= a
proof
let a; assume a in K;
then consider AA be auxiliary Relation of L such that
A8: a = AA-below x & AA in App L;
reconsider AA as approximating auxiliary Relation of L by A8,Def20;
let b be set; assume A9: b in R-below x;
R c= AA by A3;
then R-below x c= AA-below x by Th29;
hence thesis by A8,A9;
end;
then R-below x c= meet K by A5,SETFAM_1:6;
hence thesis by A4,A6,A7,XBOOLE_0:def 10;
end;
then A10: L is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
for x being Element of L holds waybelow x is non empty directed;
hence L is continuous by A10,WAYBEL_3:def 6;
end;
:: Definition 1.15 (SI) p.46
definition let L be RelStr, AR be Relation of L;
attr AR is satisfying_SI means :Def21:
for x, z be Element of L holds
( [x,z] in AR & x <> z implies
ex y be Element of L st ( [x,y] in AR & [y,z] in AR & x <> y ) );
synonym AR satisfies_SI;
end;
:: Definition 1.15 (INT) p.46
definition let L be RelStr, AR be Relation of L;
attr AR is satisfying_INT means :Def22:
for x, z be Element of L holds
( [x,z] in AR implies
ex y be Element of L st ( [x,y] in AR & [y,z] in AR ) );
synonym AR satisfies_INT;
end;
canceled;
theorem Th48:
for L being RelStr, AR being Relation of L
holds AR satisfies_SI implies AR satisfies_INT
proof
let L be RelStr, AR be Relation of L;
assume A1: AR satisfies_SI;
let x, z be Element of L;
[x,z] in AR implies ex y be Element of L st ( [x,y] in AR & [y,z] in AR )
proof
assume A2: [x,z] in AR;
per cases;
suppose x <> z;
then consider y be Element of L such that
A3: ( [x,y] in AR & [y,z] in AR & x <> y ) by A1,A2,Def21;
thus ex y be Element of L st ( [x,y] in AR & [y,z] in AR ) by A3;
suppose x = z;
hence ex y be Element of L st ( [x,y] in AR & [y,z] in AR ) by A2;
end;
hence thesis;
end;
definition let L be non empty RelStr;
cluster satisfying_SI -> satisfying_INT Relation of L;
coherence by Th48;
end;
reserve AR for Relation of L;
reserve x, y, z for Element of L;
theorem Th49:
for AR being approximating Relation of L st
not x <= y holds ex u being Element of L st [u,x] in AR & not u <= y
proof
let AR be approximating Relation of L;
assume
A1: not x <= y;
x = sup (AR-below x) & ex_sup_of (AR-below x),L
by Def18,YELLOW_0:17;
then y is_>=_than (AR-below x) implies y >= x by YELLOW_0:def 9;
then consider u being Element of L such that
A2: u in AR-below x & not u <= y by A1,LATTICE3:def 9;
take u; thus [u,x] in AR & not u <= y by A2,Th13;
end;
:: Lemma 1.16 p.46
theorem Th50:
for R being approximating auxiliary(i) auxiliary(iii) Relation of L holds
( [x,z] in R & x <> z ) implies
ex y st x <= y & [y,z] in R & x <> y
proof
let R be approximating auxiliary(i) auxiliary(iii) Relation of L;
assume A1: [x,z] in R & x <> z;
then x <= z by Def4;
then x < z by A1,ORDERS_1:def 10;
then not z < x by ORDERS_1:28;
then not z <= x by A1,ORDERS_1:def 10;
then consider u be Element of L such that
A2: [u,z] in R & not u <= x by Th49;
take y = x "\/" u;
thus x <= y by YELLOW_0:22;
thus [y,z] in R by A1,A2,Def6;
thus x <> y by A2,YELLOW_0:24;
end;
:: Lemma 1.17 p.46
theorem Th51:
for R being approximating auxiliary Relation of L holds
( x << z & x <> z ) implies
ex y being Element of L st [x,y] in R & [y,z] in R & x <> y
proof
let R be approximating auxiliary Relation of L;
assume A1: x << z & x <> z;
set I = {u where u is Element of L : ex y be Element of L st
[u,y] in R & [y,z] in R };
A2:[Bottom L,Bottom L] in R by Def7;
[Bottom L,z] in R by Def7;
then A3:Bottom L in I by A2;
I c= the carrier of L
proof let v be set; assume v in I;
then ex u1 being Element of L st v = u1 & ex y be Element of L st
[u1,y] in R & [y,z] in R;
hence thesis;
end;
then reconsider I as non empty Subset of L by A3;
A4:I is lower
proof
let x1,y1 be Element of L;
assume A5: x1 in I & y1 <= x1;
then consider v1 be Element of L such that A6: v1 = x1 &
ex s1 be Element of L st [v1,s1] in R & [s1,z] in R;
consider s1 be Element of L such that A7: [v1,s1] in R & [s1,z] in R by A6;
s1 <= s1;
then [y1, s1] in R by A5,A6,A7,Def5;
hence thesis by A7;
end;
I is directed
proof
let u1,u2 be Element of L; assume A8: u1 in I & u2 in I;
then consider v1 be Element of L such that A9: v1 = u1 &
ex y1 be Element of L st [v1,y1] in R & [y1,z] in R;
consider v2 be Element of L such that A10: v2 = u2 &
ex y2 be Element of L st [v2,y2] in R & [y2,z] in R by A8;
consider y1 be Element of L such that A11: [v1,y1] in R & [y1,z] in
R by A9;
consider y2 be Element of L such that A12: [v2,y2] in R & [y2,z] in
R by A10;
take u1 "\/" u2;
A13: [u1 "\/" u2 , y1 "\/" y2] in R by A9,A10,A11,A12,Th1;
[y1 "\/" y2 , z] in R by A11,A12,Def6;
hence thesis by A13,YELLOW_0:22;
end;
then reconsider I as Ideal of L by A4;
sup I = z
proof
set z' = sup I;
assume A14: z' <> z;
A15:I c= R-below z
proof
let a be set; assume a in I;
then consider u be Element of L such that
A16: a = u & ex y2 be Element of L st [u,y2] in R & [y2,z] in R;
consider y2 be Element of L such that A17: [u,y2] in R & [y2,z] in
R by A16;
A18: u <= y2 by A17,Def4;
z <= z;
then [u,z] in R by A17,A18,Def5;
then a in {y where y is Element of L: [y,z] in R} by A16;
hence thesis by Def11;
end;
ex_sup_of I,L & ex_sup_of (R-below z),L by YELLOW_0:17;
then A19:sup I <= sup (R-below z) by A15,YELLOW_0:34;
z = sup (R-below z) by Def18;
then z' < z by A14,A19,ORDERS_1:def 10;
then not z <= z' by ORDERS_1:30;
then consider y be Element of L such that
A20: [y, z] in R & not y <= z' by Th49;
consider u be Element of L such that
A21: [u, y] in R & not u <= z' by A20,Th49;
A22:u in I by A20,A21;
z' = "\/"(I,L) & ex_sup_of I,L iff z' is_>=_than I &
for b being Element of L st b is_>=_than I holds z' <= b by YELLOW_0:30;
hence contradiction by A21,A22,LATTICE3:def 9,YELLOW_0:17;
end;
then x in I by A1,WAYBEL_3:20;
then consider v be Element of L such that
A23: v = x & ex y' be Element of L st [v,y'] in R & [y',z] in R;
consider y' be Element of L such that A24: [v,y'] in R & [y',z] in R by A23;
A25: x <= y' by A23,A24,Def4;
z <= z;
then [x,z] in R by A24,A25,Def5;
then consider y'' be Element of L such that
A26: x <= y'' & [y'',z] in R & x <> y'' by A1,Th50;
A27: x < y'' by A26,ORDERS_1:def 10;
set Y = y' "\/" y'';
A28: y' <= Y & y'' <= Y by YELLOW_0:22;
then A29: x <> Y by A27,ORDERS_1:32;
x <= x;
then A30: [x,Y] in R by A23,A24,A28,Def5;
[Y,z] in R by A24,A26,Def6;
hence thesis by A29,A30;
end;
:: Theorem 1.18 p.47
theorem Th52:
for L being lower-bounded continuous LATTICE holds
L-waybelow satisfies_SI
proof
let L be lower-bounded continuous LATTICE;
set R = L-waybelow;
thus R satisfies_SI
proof
let x,z be Element of L;
assume A1: [x,z] in R & x <> z;
then x << z by Def2;
hence thesis by A1,Th51;
end;
end;
definition let L be lower-bounded continuous LATTICE;
cluster L-waybelow -> satisfying_SI;
coherence by Th52;
end;
theorem Th53:
for L being lower-bounded continuous LATTICE,
x,y being Element of L st x << y
ex x' being Element of L st x << x' & x' << y
proof
let L be lower-bounded continuous LATTICE;
let x,y be Element of L;
set R = L-waybelow;
assume x << y;
then [x,y] in R by Def2;
then consider x' be Element of L such that A1: [x,x'] in R & [x',y] in R
by Def22;
x << x' & x' << y by A1,Def2;
hence thesis;
end;
:: Corollary 1.19 p.47
theorem
for L being lower-bounded continuous LATTICE holds
for x,y being Element of L holds
( x << y iff
for D being non empty directed Subset of L st y <= sup D
ex d being Element of L st d in D & x << d )
proof
let L be lower-bounded continuous LATTICE;
let x,y be Element of L;
hereby assume A1: x << y;
let D be non empty directed Subset of L;
assume A2: y <= sup D;
consider x' be Element of L such that A3: x << x' & x' << y by A1,Th53;
consider d be Element of L such that
A4: d in D & x' <= d by A2,A3,WAYBEL_3:def 1;
x << d by A3,A4,WAYBEL_3:2;
hence ex d be Element of L st d in D & x << d by A4;
end;
assume A5: for D be non empty directed Subset of L st y <= sup D
ex d be Element of L st d in D & x << d;
for D being non empty directed Subset of L st y <= sup D
ex d being Element of L st d in D & x <= d
proof
let D be non empty directed Subset of L;
assume y <= sup D;
then consider d be Element of L such that A6: d in D & x << d by A5;
x <= d by A6,WAYBEL_3:1;
hence thesis by A6;
end;
hence thesis by WAYBEL_3:def 1;
end;
begin :: Exercises
definition
let L be RelStr, X be Subset of L,
R be Relation of the carrier of L;
pred X is_directed_wrt R means :Def23:
for x,y being Element of L st x in X & y in X
ex z being Element of L st z in X & [x,z] in R & [y,z] in R;
end;
theorem
for L being RelStr, X being Subset of L st
X is_directed_wrt (the InternalRel of L) holds X is directed
proof
let L be RelStr, X be Subset of L;
assume A1: X is_directed_wrt (the InternalRel of L);
let x,y be Element of L; assume x in X & y in X;
then consider z being Element of L such that
A2: z in X & [x,z] in the InternalRel of L & [y,z] in the InternalRel of L
by A1,Def23;
take z;
thus z in X by A2;
thus x <= z & y <= z by A2,ORDERS_1:def 9;
end;
definition
let X, x be set;
let R be Relation;
pred x is_maximal_wrt X,R means :Def24:
x in X & not ex y being set st y in X & y <> x & [x,y] in R;
end;
definition
let L be RelStr, X be set, x be Element of L;
pred x is_maximal_in X means :Def25:
x is_maximal_wrt X, the InternalRel of L;
end;
theorem
for L being RelStr, X being set, x being Element of L holds
x is_maximal_in X iff
x in X & not ex y being Element of L st y in X & x < y
proof
let L be RelStr, X be set, x be Element of L;
hereby assume x is_maximal_in X;
then A1:x is_maximal_wrt X, the InternalRel of L by Def25;
hence x in X by Def24;
let y be Element of L;
per cases by A1,Def24;
suppose not y in X;
hence not y in X or not x < y;
suppose y = x;
hence not y in X or not x < y;
suppose not [x,y] in the InternalRel of L;
then not x <= y by ORDERS_1:def 9;
hence not y in X or not x < y by ORDERS_1:def 10;
end;
assume A2: x in X & not ex y be Element of L st y in X & x < y;
assume not x is_maximal_in X;
then not x is_maximal_wrt X, the InternalRel of L by Def25;
then consider y be set such that
A3: y in X & y <> x & [x,y] in the InternalRel of L by A2,Def24;
y in the carrier of L by A3,ZFMISC_1:106;
then reconsider y as Element of L;
x <= y by A3,ORDERS_1:def 9;
then x < y by A3,ORDERS_1:def 10;
hence thesis by A2,A3;
end;
definition
let X, x be set;
let R be Relation;
pred x is_minimal_wrt X,R means :Def26:
x in X & not ex y being set st y in X & y <> x & [y,x] in R;
end;
definition
let L be RelStr, X be set, x be Element of L;
pred x is_minimal_in X means :Def27:
x is_minimal_wrt X, the InternalRel of L;
end;
theorem
for L being RelStr, X being set, x being Element of L holds
x is_minimal_in X iff
x in X & not ex y being Element of L st y in X & x > y
proof
let L be RelStr, X be set, x be Element of L;
hereby assume x is_minimal_in X;
then A1: x is_minimal_wrt X, the InternalRel of L by Def27;
hence x in X by Def26;
let y be Element of L;
per cases by A1,Def26;
suppose not y in X;
hence not y in X or not x > y;
suppose y = x;
hence not y in X or not x > y;
suppose not [y,x] in the InternalRel of L;
then not y <= x by ORDERS_1:def 9;
hence not y in X or not y < x by ORDERS_1:def 10;
end;
assume A2: x in X & not ex y be Element of L st y in X & x > y;
assume not x is_minimal_in X;
then not x is_minimal_wrt X, the InternalRel of L by Def27;
then consider y be set such that
A3: y in X & y <> x & [y,x] in the InternalRel of L by A2,Def26;
y in the carrier of L by A3,ZFMISC_1:106;
then reconsider y as Element of L;
y <= x by A3,ORDERS_1:def 9;
then y < x by A3,ORDERS_1:def 10;
hence thesis by A2,A3;
end;
:: Exercise 1.23 (i) ( 1 => 2 )
theorem
AR satisfies_SI implies
( for x holds ( ex y st y is_maximal_wrt (AR-below x), AR )
implies [x,x] in AR )
proof
assume A1: AR satisfies_SI;
let x;
given y such that A2: y is_maximal_wrt (AR-below x), AR;
A3: y in AR-below x & not ex y' be Element of L st
y' in AR-below x & y <> y' & [y,y'] in AR by A2,Def24;
assume A4: not [x,x] in AR;
A5: [y,x] in AR by A3,Th13;
per cases;
suppose x = y;
hence contradiction by A3,A4,Th13;
suppose x <> y;
then consider z such that A6: [y,z] in AR & [z,x] in AR & z <> y by A1,A5,
Def21;
z in AR-below x by A6,Th13;
hence contradiction by A2,A6,Def24;
end;
:: Exercise 1.23 (i) ( 2 => 1 )
theorem
( for x holds ( ex y st y is_maximal_wrt (AR-below x), AR )
implies [x,x] in AR ) implies AR satisfies_SI
proof
assume A1: for x holds ( ex y st y is_maximal_wrt (AR-below x), AR )
implies [x,x] in AR;
now let z,x; assume A2: [z,x] in AR & z <> x;
then A3: z in AR-below x by Th13;
per cases;
suppose [x,x] in AR;
hence ex y st ( [z,y] in AR & [y,x] in AR & z <> y ) by A2;
suppose not [x,x] in AR;
then not z is_maximal_wrt (AR-below x), AR by A1;
then consider y being set such that
A4: y in AR-below x & y <> z & [z,y] in AR by A3,Def24;
[y,x] in AR by A4,Th13;
hence ex y st [z,y] in AR & [y,x] in AR & z <> y by A4;
end;
hence thesis by Def21;
end;
:: Exercise 1.23 (ii) ( 3 => 4 )
theorem
for AR being auxiliary(ii) auxiliary(iii) Relation of L holds
AR satisfies_INT implies
( for x holds AR-below x is_directed_wrt AR)
proof
let AR be auxiliary(ii) auxiliary(iii) Relation of L;
assume A1: AR satisfies_INT;
let x,y,z;
assume y in AR-below x & z in AR-below x;
then A2: [y,x] in AR & [z,x] in AR by Th13;
then consider y' be Element of L such that
A3: [y,y'] in AR & [y',x] in AR by A1,Def22;
consider z' be Element of L such that
A4: [z,z'] in AR & [z',x] in AR by A1,A2,Def22;
take u = y' "\/" z';
[u,x] in AR by A3,A4,Def6;
hence u in AR-below x by Th13;
y <= y & y' <= u by YELLOW_0:22;
hence [y,u] in AR by A3,Def5;
z <= z & z' <= u by YELLOW_0:22;
hence [z,u] in AR by A4,Def5;
end;
:: Exercise 1.23 (ii) ( 4 => 3 )
theorem
( for x holds AR-below x is_directed_wrt AR) implies AR satisfies_INT
proof
assume A1: for x holds AR-below x is_directed_wrt AR;
let X,Z be Element of L;
assume [X,Z] in AR;
then A2: X in AR-below Z by Th13;
AR-below Z is_directed_wrt AR by A1;
then consider u be Element of L such that
A3: u in AR-below Z & [X,u] in AR & [X,u] in AR by A2,Def23;
take u;
thus [X,u] in AR by A3;
thus [u,Z] in AR by A3,Th13;
end;
:: Exercise 1.23 (iii) p.51
theorem Th62:
for R being approximating auxiliary(i) auxiliary(ii) auxiliary(iii)
Relation of L st
R satisfies_INT holds R satisfies_SI
proof
let R be approximating auxiliary(i) auxiliary(ii) auxiliary(iii)
Relation of L;
assume A1: R satisfies_INT;
let x, z;
assume A2: [x,z] in R & x <> z;
then consider y such that A3: ( [x,y] in R & [y,z] in R ) by A1,Def22;
consider y' be Element of L such that A4: x <= y' & [y',z] in R & x <> y'
by A2,Th50;
A5: x < y' by A4,ORDERS_1:def 10;
take Y = y "\/" y';
A6: x <= y by A3,Def4;
A7: x <= x & y <= Y by YELLOW_0:22;
per cases;
suppose y' <= y;
then x < y by A5,ORDERS_1:32;
hence thesis by A3,A4,A7,Def5,Def6,ORDERS_1:32;
suppose not y' <= y;
then y <> Y by YELLOW_0:24;
then y < Y by A7,ORDERS_1:def 10;
hence thesis by A3,A4,A6,A7,Def5,Def6,ORDERS_1:32;
end;
definition let L;
cluster satisfying_INT ->
satisfying_SI (approximating auxiliary Relation of L);
coherence by Th62;
end;