begin
:: deftheorem WAYBEL_4:def 1 :
canceled;
:: deftheorem Def2 defines -waybelow WAYBEL_4:def 2 :
:: deftheorem defines IntRel WAYBEL_4:def 3 :
:: deftheorem Def4 defines auxiliary(i) WAYBEL_4:def 4 :
:: deftheorem Def5 defines auxiliary(ii) WAYBEL_4:def 5 :
:: deftheorem Def6 defines auxiliary(iii) WAYBEL_4:def 6 :
:: deftheorem Def7 defines auxiliary(iv) WAYBEL_4:def 7 :
:: deftheorem Def8 defines auxiliary WAYBEL_4:def 8 :
theorem Th1:
Lm1:
for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) auxiliary(ii) Relation of holds AR is transitive
:: deftheorem Def9 defines Aux WAYBEL_4:def 9 :
Lm2:
for L being lower-bounded sup-Semilattice
for AR being auxiliary(i) Relation of
for a, b being set st [a,b] in AR holds
[a,b] in IntRel L
theorem Th2:
theorem
:: deftheorem Def10 defines AuxBottom WAYBEL_4:def 10 :
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
:: deftheorem defines -below WAYBEL_4:def 11 :
:: deftheorem defines -above WAYBEL_4:def 12 :
theorem Th12:
:: deftheorem Def13 defines -below WAYBEL_4:def 13 :
theorem Th13:
theorem
Lm3:
for L being lower-bounded with_suprema Poset
for AR being Relation of
for a being set
for y being Element of holds
( a in downarrow y iff [a,y] in the InternalRel of L )
theorem
definition
let L be non
empty Poset;
func MonSet L -> strict RelStr means :
Def14:
for
a being
set holds
( (
a in the
carrier of
it implies ex
s being
Function of
L,
(InclPoset (Ids L)) st
(
a = s &
s is
monotone & ( for
x being
Element of 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 holds
s . x c= downarrow x ) ) implies
a in the
carrier of
it ) & ( for
c,
d being
set holds
(
[c,d] in the
InternalRel of
it iff ex
f,
g being
Function 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
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 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 holds s . x c= downarrow x ) ) implies a in the carrier of b1 ) & ( for c, d being set 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 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 holds s . x c= downarrow x ) ) implies a in the carrier of b1 ) & ( for c, d being set 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 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 holds s . x c= downarrow x ) ) implies a in the carrier of b2 ) & ( for c, d being set 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;
:: deftheorem Def14 defines MonSet WAYBEL_4:def 14 :
theorem
theorem Th17:
theorem Th18:
theorem Th19:
theorem
theorem Th21:
theorem
theorem Th23:
theorem
Lm4:
for L being lower-bounded sup-Semilattice
for I being Ideal of L holds {(Bottom L)} c= I
theorem Th25:
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
theorem Th26:
theorem
Lm6:
for L being lower-bounded sup-Semilattice ex x being Element of st x is_>=_than the carrier of (MonSet L)
:: deftheorem Def15 defines Rel2Map WAYBEL_4:def 15 :
theorem
theorem Th29:
Lm7:
for L being lower-bounded sup-Semilattice holds Rel2Map L is monotone
definition
let L be
lower-bounded sup-Semilattice;
func Map2Rel L -> Function of
(MonSet L),
(InclPoset (Aux L)) means :
Def16:
for
s being
set st
s in the
carrier of
(MonSet L) holds
ex
AR being
auxiliary Relation of st
(
AR = it . s & ( for
x,
y being
set holds
(
[x,y] in AR iff ex
x',
y' being
Element of ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
x' = x &
y' = y &
s' = s &
x' in s' . y' ) ) ) );
existence
ex b1 being Function of (MonSet L),(InclPoset (Aux L)) st
for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of st
( AR = b1 . s & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) )
uniqueness
for b1, b2 being Function of (MonSet L),(InclPoset (Aux L)) st ( for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of st
( AR = b1 . s & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) ) ) & ( for s being set st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of st
( AR = b2 . s & ( for x, y being set holds
( [x,y] in AR iff ex x', y' being Element of ex s' being Function of L,(InclPoset (Ids L)) st
( x' = x & y' = y & s' = s & x' in s' . y' ) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def16 defines Map2Rel WAYBEL_4:def 16 :
Lm8:
for L being lower-bounded sup-Semilattice holds Map2Rel L is monotone
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem Th34:
:: deftheorem Def17 defines DownMap WAYBEL_4:def 17 :
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
for I being Ideal of L holds (DownMap I) . x c= downarrow x
theorem Th35:
theorem Th36:
begin
:: deftheorem Def18 defines approximating WAYBEL_4:def 18 :
:: deftheorem Def19 defines approximating WAYBEL_4:def 19 :
theorem Th37:
Lm11:
for L being complete LATTICE
for x being Element of
for D being directed Subset of holds sup ({x} "/\" D) <= x
theorem Th38:
theorem
theorem Th40:
theorem Th41:
Lm12:
for L being lower-bounded continuous LATTICE holds L -waybelow is approximating
:: deftheorem Def20 defines App WAYBEL_4:def 20 :
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem
:: deftheorem Def21 defines satisfying_SI WAYBEL_4:def 21 :
:: deftheorem Def22 defines satisfying_INT WAYBEL_4:def 22 :
theorem
canceled;
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem
begin
:: deftheorem Def23 defines is_directed_wrt WAYBEL_4:def 23 :
theorem
:: deftheorem Def24 defines is_maximal_wrt WAYBEL_4:def 24 :
:: deftheorem Def25 defines is_maximal_in WAYBEL_4:def 25 :
theorem
:: deftheorem Def26 defines is_minimal_wrt WAYBEL_4:def 26 :
:: deftheorem Def27 defines is_minimal_in WAYBEL_4:def 27 :
theorem
theorem
theorem
theorem
theorem
theorem Th62: