environ
vocabularies HIDDEN, XBOOLE_0, RELAT_2, ORDERS_2, RELAT_1, SUBSET_1, WAYBEL_3, STRUCT_0, XXREAL_0, EQREL_1, LATTICES, LATTICE3, WAYBEL_0, TARSKI, ZFMISC_1, YELLOW_1, SETFAM_1, REWRITE1, YELLOW_0, FUNCT_1, CARD_FIL, SEQM_3, PARTFUN1, CAT_1, NEWTON, FUNCOP_1, FUNCT_2, CARD_3, RLVECT_2, WELLORD1, YELLOW_2, WELLORD2, ORDINAL2, WAYBEL_2, ARYTM_3, ORDERS_1, WAYBEL_4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, ORDERS_1, STRUCT_0, ORDERS_2, LATTICE3, WELLORD1, YELLOW_0, FUNCOP_1, CARD_3, PRALG_1, YELLOW_1, ALG_1, YELLOW_2, YELLOW_4, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_3;
definitions LATTICE3, XBOOLE_0, TARSKI, YELLOW_0, WAYBEL_0, RELAT_1, YELLOW_2, ORDERS_3;
theorems FUNCOP_1, FUNCT_1, FUNCT_2, LATTICE3, ORDERS_2, PARTFUN1, RELAT_1, RELAT_2, RELSET_1, SETFAM_1, TARSKI, WAYBEL_0, WAYBEL_3, WAYBEL_2, WELLORD2, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_4, ZFMISC_1, XBOOLE_0, XBOOLE_1;
schemes FUNCT_2, PARTFUN1, RELSET_1, XBOOLE_0, XFAMILY;
registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_2, WAYBEL_3, FUNCOP_1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, TOLER_1, PRALG_1, ORDERS_3, WAYBEL_1, YELLOW_4, WAYBEL_2, WAYBEL_3, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0, YELLOW_0, WAYBEL_0, WELLORD1, STRUCT_0;
expansions LATTICE3, XBOOLE_0, TARSKI, YELLOW_0, RELAT_1, YELLOW_2, ORDERS_3;
Lm1:
for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) auxiliary(ii) Relation of L holds AR is transitive
Lm2:
for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) Relation of L
for a, b being object st [a,b] in AR holds
[a,b] in IntRel L
Lm3:
for L being lower-bounded with_suprema Poset
for AR being Relation of L
for a being set
for y being Element of L holds
( a in downarrow y iff [a,y] in the InternalRel of L )
definition
let L be non
empty Poset;
existence
ex b1 being strict RelStr st
for a being set holds
( ( a in the carrier of b1 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b1 ) & ( for c, d being object holds
( [c,d] in the InternalRel of b1 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b1 & d in the carrier of b1 & f <= g ) ) ) )
uniqueness
for b1, b2 being strict RelStr st ( for a being set holds
( ( a in the carrier of b1 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b1 ) & ( for c, d being object holds
( [c,d] in the InternalRel of b1 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b1 & d in the carrier of b1 & f <= g ) ) ) ) ) & ( for a being set holds
( ( a in the carrier of b2 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of b2 ) & ( for c, d being object holds
( [c,d] in the InternalRel of b2 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of b2 & d in the carrier of b2 & f <= g ) ) ) ) ) holds
b1 = b2
end;
Lm4:
for L being lower-bounded sup-Semilattice
for I being Ideal of L holds {(Bottom L)} c= I
Lm5:
for L being lower-bounded sup-Semilattice
for f being Function of L,(InclPoset (Ids L)) st f = the carrier of L --> {(Bottom L)} holds
f is monotone
Lm6:
for L being lower-bounded sup-Semilattice ex x being Element of (MonSet L) st x is_>=_than the carrier of (MonSet L)
Lm7:
for L being lower-bounded sup-Semilattice holds Rel2Map L is monotone
definition
let L be
lower-bounded sup-Semilattice;
existence
ex b1 being Function of (MonSet L),(InclPoset (Aux L)) st
for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b1 . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
uniqueness
for b1, b2 being Function of (MonSet L),(InclPoset (Aux L)) st ( for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b1 . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) & ( for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b2 . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) ) holds
b1 = b2
end;
Lm8:
for L being lower-bounded sup-Semilattice holds Map2Rel L is monotone
Lm9:
for L being Semilattice
for I being Ideal of L holds DownMap I is monotone
Lm10:
for L being Semilattice
for x being Element of L
for I being Ideal of L holds (DownMap I) . x c= downarrow x
Lm11:
for L being complete LATTICE
for x being Element of L
for D being directed Subset of L holds sup ({x} "/\" D) <= x
Lm12:
for L being lower-bounded continuous LATTICE holds L -waybelow is approximating