begin
Lemiter01:
for f being Function st rng f c= dom f holds
iter (f,0) = id (dom f)
Lemiter02:
for f being Function
for n being Nat st rng f c= dom f holds
( dom (iter (f,n)) = dom f & rng (iter (f,n)) c= dom f )
Lemiter03:
for X being set
for f being Function of X,X
for n being Nat holds iter (f,n) is Function of X,X
LemMin01:
for A being non empty RelStr
for a being Element of A holds
( a is_<=_than the carrier of A iff for x being Element of A holds a <= x )
:: deftheorem DefchainComplete defines chain-complete POSET_1:def 1 :
for IT being RelStr holds
( IT is chain-complete iff ( IT is lower-bounded & ( for L being Chain of IT st not L is empty holds
ex_sup_of L,IT ) ) );
theorem ThChain1:
theorem Thmonotone02:
begin
Lemiter10:
for P being non empty Poset
for g being monotone Function of P,P
for p being Element of P holds (iter (g,0)) . p = p
:: deftheorem defines iterSet POSET_1:def 2 :
for P being non empty Poset
for g being monotone Function of P,P
for p being Element of P holds iterSet (g,p) = { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } ;
Lemiter11:
for n being Nat
for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P holds (iter (g,n)) . p is Element of P
Lemiter12:
for n being Nat
for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P holds
( (g * (iter (g,n))) . p = g . ((iter (g,n)) . p) & ((iter (g,n)) * g) . p = (iter (g,n)) . (g . p) )
Lemiter13:
for n being Nat
for P being non empty strict chain-complete Poset
for p, p3, p1, p4 being Element of P
for g being monotone Function of P,P st p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,n)) . p3 holds
p1 <= p4
Lemiter14:
for n, k being Nat
for P being non empty strict chain-complete Poset
for p3, p, p1, p4 being Element of P
for g being monotone Function of P,P st p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,(n + k))) . p holds
p1 <= p4
Lemiter15:
for n, m being Nat
for P being non empty strict chain-complete Poset
for p3, p, p1, p4 being Element of P
for g being monotone Function of P,P st n <= m & p3 = g . p & p <= p3 & p1 = (iter (g,n)) . p & p4 = (iter (g,m)) . p holds
p1 <= p4
Lemiter16:
for n being Nat
for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P st p is_a_fixpoint_of g holds
(iter (g,n)) . p = p
Lemiter17:
for n being Nat
for P being non empty strict chain-complete Poset
for p1, p, p2 being Element of P
for g1, g2 being monotone Function of P,P st g1 <= g2 & p1 = (iter (g1,n)) . p & p2 = (iter (g2,n)) . p holds
p1 <= p2
theorem ThiterSet1:
:: deftheorem defines iter_min POSET_1:def 3 :
for P being non empty strict chain-complete Poset
for g being monotone Function of P,P holds iter_min g = iterSet (g,(Bottom P));
theorem ThiterSet2:
theorem ThiterSet3:
:: deftheorem Defcontinuous defines continuous POSET_1:def 4 :
for P, Q being non empty Poset
for f being Function of P,Q holds
( f is continuous iff ( f is monotone & ( for L being non empty Chain of P holds f preserves_sup_of L ) ) );
theorem Thcontinuous01:
theorem Thcontinuous02:
theorem Thcontinuous03:
Lemfixpoint01:
for P being non empty strict chain-complete Poset
for p being Element of P
for g being monotone Function of P,P st g is continuous & p = sup (iter_min g) holds
p is_a_fixpoint_of g
Lemfixpoint02:
for P being non empty strict chain-complete Poset
for p4 being Element of P
for g being monotone Function of P,P st p4 = sup (iter_min g) holds
for p being Element of P st p is_a_fixpoint_of g holds
p4 <= p
:: deftheorem Defleastfixpoint defines least_fix_point POSET_1:def 5 :
for P being non empty strict chain-complete Poset
for g being monotone Function of P,P st g is continuous holds
for b3 being Element of P holds
( b3 = least_fix_point g iff ( b3 is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds
b3 <= p ) ) );
theorem Thfixpoint01:
theorem Thfixpoint02:
begin
:: deftheorem defines ConFuncs POSET_1:def 6 :
for P, Q being non empty strict chain-complete Poset holds ConFuncs (P,Q) = { x where x is Element of Funcs ( the carrier of P, the carrier of Q) : ex f being continuous Function of P,Q st f = x } ;
Lemlessthan01:
for P, Q being non empty strict chain-complete Poset
for f being Function of P,Q holds f <= f
Lemlessthan02:
for P, Q being non empty strict chain-complete Poset
for f, g, h being Function of P,Q st f <= g & g <= h holds
f <= h
Lemlessthan03:
for P, Q being non empty strict chain-complete Poset
for f, g being Function of P,Q st f <= g & g <= f holds
f = g
definition
let P,
Q be non
empty strict chain-complete Poset;
func ConRelat (
P,
Q)
-> Relation of
(ConFuncs (P,Q)) means :
DefConRelat:
for
x,
y being
set holds
(
[x,y] in it iff (
x in ConFuncs (
P,
Q) &
y in ConFuncs (
P,
Q) & ex
f,
g being
Function of
P,
Q st
(
x = f &
y = g &
f <= g ) ) );
existence
ex b1 being Relation of (ConFuncs (P,Q)) st
for x, y being set holds
( [x,y] in b1 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) )
uniqueness
for b1, b2 being Relation of (ConFuncs (P,Q)) st ( for x, y being set holds
( [x,y] in b1 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) ) holds
b1 = b2
end;
:: deftheorem DefConRelat defines ConRelat POSET_1:def 7 :
for P, Q being non empty strict chain-complete Poset
for b3 being Relation of (ConFuncs (P,Q)) holds
( b3 = ConRelat (P,Q) iff for x, y being set holds
( [x,y] in b3 iff ( x in ConFuncs (P,Q) & y in ConFuncs (P,Q) & ex f, g being Function of P,Q st
( x = f & y = g & f <= g ) ) ) );
LemConRelat01:
for P, Q being non empty strict chain-complete Poset holds field (ConRelat (P,Q)) c= ConFuncs (P,Q)
LemConRelat02:
for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q)
LemConRelat03:
for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_transitive_in ConFuncs (P,Q)
LemConRelat04:
for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_antisymmetric_in ConFuncs (P,Q)
:: deftheorem defines ConPoset POSET_1:def 8 :
for P, Q being non empty strict chain-complete Poset holds ConPoset (P,Q) = RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #);
:: deftheorem defines -image POSET_1:def 9 :
for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q))
for p being Element of P holds F -image p = { x where x is Element of Q : ex f being continuous Function of P,Q st
( f in F & x = f . p ) } ;
:: deftheorem Defsupfunc defines sup_func POSET_1:def 10 :
for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q))
for b4 being Function of P,Q holds
( b4 = sup_func F iff for p being Element of P
for M being non empty Chain of Q st M = F -image p holds
b4 . p = sup M );
Lemsup01:
for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is monotone
Lem201:
for Q being non empty strict chain-complete Poset
for M being non empty Chain of Q
for q being Element of Q st q in M holds
q <= sup M
Lem202:
for Q being non empty strict chain-complete Poset
for M being non empty Chain of Q
for q1 being Element of Q st ( for q being Element of Q st q in M holds
q <= q1 ) holds
sup M <= q1
Lemsup02:
for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is continuous
Lemsup03:
for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds sup_func F is Element of (ConPoset (P,Q))
Lem301:
for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q))
for x being set st x in F holds
ex g being continuous Function of P,Q st x = g
theorem ThConPoset01:
:: deftheorem defines min_func POSET_1:def 11 :
for P, Q being non empty strict chain-complete Poset holds min_func (P,Q) = P --> (Bottom Q);
LemMinFunc01:
for P, Q being non empty strict chain-complete Poset holds min_func (P,Q) is Element of (ConPoset (P,Q))
theorem ThConPoset02:
begin
LemCastFunc01:
for x being set
for P being non empty strict chain-complete Poset st x is Element of (ConPoset (P,P)) holds
x is continuous Function of P,P
LemCastFunc02:
for P being non empty strict chain-complete Poset
for g being monotone Function of P,P st g is continuous Function of P,P holds
g is Element of (ConPoset (P,P))
definition
let P be non
empty strict chain-complete Poset;
func fix_func P -> Function of
(ConPoset (P,P)),
P means :
Deffixfunc:
for
g being
Element of
(ConPoset (P,P)) for
h being
continuous Function of
P,
P st
g = h holds
it . g = least_fix_point h;
existence
ex b1 being Function of (ConPoset (P,P)),P st
for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b1 . g = least_fix_point h
uniqueness
for b1, b2 being Function of (ConPoset (P,P)),P st ( for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b1 . g = least_fix_point h ) & ( for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b2 . g = least_fix_point h ) holds
b1 = b2
end;
:: deftheorem Deffixfunc defines fix_func POSET_1:def 12 :
for P being non empty strict chain-complete Poset
for b2 being Function of (ConPoset (P,P)),P holds
( b2 = fix_func P iff for g being Element of (ConPoset (P,P))
for h being continuous Function of P,P st g = h holds
b2 . g = least_fix_point h );
LemFix01:
for P being non empty strict chain-complete Poset
for p1, p2 being Element of (ConPoset (P,P)) st p1 <= p2 holds
( p1 in ConFuncs (P,P) & p2 in ConFuncs (P,P) & ex g1, g2 being continuous Function of P,P st
( p1 = g1 & p2 = g2 & g1 <= g2 ) )
LemFix0201:
for P being non empty strict chain-complete Poset holds fix_func P is monotone Function of (ConPoset (P,P)),P
LemFix02:
for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X, x being set st X = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) } & x in X holds
ex p being Element of P ex g being continuous Function of P,P st
( x = p & g in G & p = (iter (g,n)) . (Bottom P) )
LemFix0301:
for x being set
for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) } & x in X holds
x is Element of P
LemFix03:
for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) } holds
X is non empty Subset of P
LemFix0401:
for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for f, g being monotone Function of P,P st f in G & g in G & not f <= g holds
g <= f
LemFix04:
for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for n being Nat
for X being set st X = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) } holds
X is non empty Chain of P
LemFix0503:
for P being non empty strict chain-complete Poset
for h being Function of (ConPoset (P,P)),P
for G being non empty Chain of (ConPoset (P,P))
for x being set st x in G holds
h . x in h .: G
LemFix0504:
for P being non empty strict chain-complete Poset
for g being continuous Function of P,P
for p, p1 being Element of P
for n being Nat st p = (fix_func P) . g & p1 = (iter (g,n)) . (Bottom P) holds
p1 <= p
LemFix0505:
for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P))
for x being set
for n being Nat
for M being non empty Chain of P
for g1 being monotone Function of P,P st M = { p where p is Element of P : ex g being Element of (ConPoset (P,P)) ex h being continuous Function of P,P st
( h = g & g in G & p = (iter (h,n)) . (Bottom P) ) } & x in g1 .: M holds
ex g being continuous Function of P,P st
( g in G & x = g1 . ((iter (g,n)) . (Bottom P)) )
LemFix05:
for P being non empty strict chain-complete Poset
for G being non empty Chain of (ConPoset (P,P)) holds (fix_func P) . (sup G) <= sup ((fix_func P) .: G)