:: by Kazuhisa Ishida and Yasunari Shidama

::

:: Received November 10, 2009

:: Copyright (c) 2009-2018 Association of Mizar Users

registration
end;

definition

let IT be RelStr ;

end;
attr IT is chain-complete means :Def1: :: POSET_1:def 1

( IT is lower-bounded & ( for L being Chain of IT st not L is empty holds

ex_sup_of L,IT ) );

( IT is lower-bounded & ( for L being Chain of IT st not L is empty holds

ex_sup_of L,IT ) );

:: deftheorem Def1 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 ) ) );

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 Th1: :: POSET_1:1

for P1, P2 being non empty Poset

for K being non empty Chain of P1

for h being monotone Function of P1,P2 holds h .: K is non empty Chain of P2

for K being non empty Chain of P1

for h being monotone Function of P1,P2 holds h .: K is non empty Chain of P2

proof end;

registration

existence

ex b_{1} being Poset st

( b_{1} is strict & b_{1} is chain-complete & not b_{1} is empty )

end;
ex b

( b

proof end;

registration
end;

:: Minimum and sup.

theorem Th2: :: POSET_1:2

for P, Q being non empty strict chain-complete Poset

for L being non empty Chain of P

for f being monotone Function of P,Q holds sup (f .: L) <= f . (sup L)

for L being non empty Chain of P

for f being monotone Function of P,Q holds sup (f .: L) <= f . (sup L)

proof end;

Lm1: 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

proof end;

definition

let P be non empty Poset;

let g be monotone Function of P,P;

let p be Element of P;

coherence

{ x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } is non empty set ;

end;
let g be monotone Function of P,P;

let p be Element of P;

func iterSet (g,p) -> non empty set equals :: POSET_1:def 2

{ x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } ;

correctness { x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } ;

coherence

{ x where x is Element of P : ex n being Nat st x = (iter (g,n)) . p } is non empty set ;

proof end;

:: 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 } ;

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 } ;

Lm2: 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) )

by FUNCT_2:15;

Lm3: for n being Nat

for P being non empty strict chain-complete Poset

for p, p1, p3, 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

proof end;

Lm4: for n, k being Nat

for P being non empty strict chain-complete Poset

for p, p1, p3, 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

proof end;

Lm5: for n, m being Nat

for P being non empty strict chain-complete Poset

for p, p1, p3, 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

proof end;

Lm6: 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

proof end;

Lm7: for n being Nat

for P being non empty strict chain-complete Poset

for p, p1, 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

proof end;

theorem Th3: :: POSET_1:3

for P being non empty strict chain-complete Poset

for g being monotone Function of P,P holds iterSet (g,(Bottom P)) is non empty Chain of P

for g being monotone Function of P,P holds iterSet (g,(Bottom P)) is non empty Chain of P

proof end;

definition

let P be non empty strict chain-complete Poset;

let g be monotone Function of P,P;

correctness

coherence

iterSet (g,(Bottom P)) is non empty Chain of P;

by Th3;

end;
let g be monotone Function of P,P;

correctness

coherence

iterSet (g,(Bottom P)) is non empty Chain of P;

by Th3;

:: 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));

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 Th4: :: POSET_1:4

for P being non empty strict chain-complete Poset

for g being monotone Function of P,P holds sup (iter_min g) = sup (g .: (iter_min g))

for g being monotone Function of P,P holds sup (iter_min g) = sup (g .: (iter_min g))

proof end;

theorem Th5: :: POSET_1:5

for P being non empty strict chain-complete Poset

for g1, g2 being monotone Function of P,P st g1 <= g2 holds

sup (iter_min g1) <= sup (iter_min g2)

for g1, g2 being monotone Function of P,P st g1 <= g2 holds

sup (iter_min g1) <= sup (iter_min g2)

proof end;

:: Continuous function on chain-complete Poset

definition

let P, Q be non empty Poset;

let f be Function of P,Q;

end;
let f be Function of P,Q;

attr f is continuous means :: POSET_1:def 4

( f is monotone & ( for L being non empty Chain of P holds f preserves_sup_of L ) );

( f is monotone & ( for L being non empty Chain of P holds f preserves_sup_of L ) );

:: deftheorem 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 ) ) );

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 Th6: :: POSET_1:6

for P, Q being non empty strict chain-complete 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 . (sup L) = sup (f .: L) ) ) )

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 . (sup L) = sup (f .: L) ) ) )

proof end;

theorem Th7: :: POSET_1:7

for P, Q being non empty strict chain-complete Poset

for z being Element of Q holds P --> z is continuous

for z being Element of Q holds P --> z is continuous

proof end;

registration

let P, Q be non empty strict chain-complete Poset;

ex b_{1} being Function of P,Q st b_{1} is continuous

end;
cluster Relation-like the carrier of P -defined the carrier of Q -valued Function-like quasi_total continuous for Function of ,;

existence ex b

proof end;

registration

let P, Q be non empty strict chain-complete Poset;

correctness

coherence

for b_{1} being Function of P,Q st b_{1} is continuous holds

b_{1} is monotone ;

;

end;
correctness

coherence

for b

b

;

theorem Th8: :: POSET_1:8

for P, Q being non empty strict chain-complete Poset

for f being monotone Function of P,Q st ( for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ) holds

f is continuous

for f being monotone Function of P,Q st ( for L being non empty Chain of P holds f . (sup L) <= sup (f .: L) ) holds

f is continuous

proof end;

Lm8: 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

proof end;

Lm9: 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

proof end;

definition

let P be non empty strict chain-complete Poset;

let g be monotone Function of P,P;

assume A1: g is continuous ;

ex b_{1} being Element of P st

( b_{1} is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds

b_{1} <= p ) )

for b_{1}, b_{2} being Element of P st b_{1} is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds

b_{1} <= p ) & b_{2} is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds

b_{2} <= p ) holds

b_{1} = b_{2}

end;
let g be monotone Function of P,P;

assume A1: g is continuous ;

func least_fix_point g -> Element of P means :Def5: :: POSET_1:def 5

( it is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds

it <= p ) );

existence ( it is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds

it <= p ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 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 b_{3} being Element of P holds

( b_{3} = least_fix_point g iff ( b_{3} is_a_fixpoint_of g & ( for p being Element of P st p is_a_fixpoint_of g holds

b_{3} <= p ) ) );

for P being non empty strict chain-complete Poset

for g being monotone Function of P,P st g is continuous holds

for b

( b

b

theorem Th9: :: POSET_1:9

for P being non empty strict chain-complete Poset

for g being continuous Function of P,P holds least_fix_point g = sup (iter_min g)

for g being continuous Function of P,P holds least_fix_point g = sup (iter_min g)

proof end;

theorem Th10: :: POSET_1:10

for P being non empty strict chain-complete Poset

for g1, g2 being continuous Function of P,P st g1 <= g2 holds

least_fix_point g1 <= least_fix_point g2

for g1, g2 being continuous Function of P,P st g1 <= g2 holds

least_fix_point g1 <= least_fix_point g2

proof end;

:: 3. Function space of continuous functions on chain-complete Posets

definition

let P, Q be non empty strict chain-complete Poset;

coherence

{ 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 } is non empty set ;

end;
func ConFuncs (P,Q) -> non empty set equals :: POSET_1:def 6

{ 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 } ;

correctness { 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 } ;

coherence

{ 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 } is non empty set ;

proof end;

:: 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 } ;

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 } ;

Lm10: for P, Q being non empty strict chain-complete Poset

for f being Function of P,Q holds f <= f

proof end;

Lm11: 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

proof end;

Lm12: 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

proof end;

definition

let P, Q be non empty strict chain-complete Poset;

ex b_{1} being Relation of (ConFuncs (P,Q)) st

for x, y being set holds

( [x,y] in b_{1} 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 b_{1}, b_{2} being Relation of (ConFuncs (P,Q)) st ( for x, y being set holds

( [x,y] in b_{1} 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 b_{2} 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

b_{1} = b_{2}

end;
func ConRelat (P,Q) -> Relation of (ConFuncs (P,Q)) means :Def7: :: POSET_1:def 7

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 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 ) ) );

ex b

for x, y being set holds

( [x,y] in b

( x = f & y = g & f <= g ) ) )

proof end;

uniqueness for b

( [x,y] in b

( x = f & y = g & f <= g ) ) ) ) & ( for x, y being set holds

( [x,y] in b

( x = f & y = g & f <= g ) ) ) ) holds

b

proof end;

:: deftheorem Def7 defines ConRelat POSET_1:def 7 :

for P, Q being non empty strict chain-complete Poset

for b_{3} being Relation of (ConFuncs (P,Q)) holds

( b_{3} = ConRelat (P,Q) iff for x, y being set holds

( [x,y] in b_{3} 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 P, Q being non empty strict chain-complete Poset

for b

( b

( [x,y] in b

( x = f & y = g & f <= g ) ) ) );

Lm13: for P, Q being non empty strict chain-complete Poset holds field (ConRelat (P,Q)) c= ConFuncs (P,Q)

proof end;

Lm14: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_reflexive_in ConFuncs (P,Q)

proof end;

Lm15: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_transitive_in ConFuncs (P,Q)

proof end;

Lm16: for P, Q being non empty strict chain-complete Poset holds ConRelat (P,Q) is_antisymmetric_in ConFuncs (P,Q)

proof end;

registration

let P, Q be non empty strict chain-complete Poset;

coherence

ConRelat (P,Q) is reflexive

ConRelat (P,Q) is transitive

ConRelat (P,Q) is antisymmetric

end;
coherence

ConRelat (P,Q) is reflexive

proof end;

coherence ConRelat (P,Q) is transitive

proof end;

coherence ConRelat (P,Q) is antisymmetric

proof end;

definition

let P, Q be non empty strict chain-complete Poset;

coherence

RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is non empty strict Poset;

by Lm14, Lm15, Lm16, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

end;
func ConPoset (P,Q) -> non empty strict Poset equals :: POSET_1:def 8

RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #);

correctness RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #);

coherence

RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #) is non empty strict Poset;

by Lm14, Lm15, Lm16, ORDERS_2:def 2, ORDERS_2:def 3, ORDERS_2:def 4;

:: 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)) #);

for P, Q being non empty strict chain-complete Poset holds ConPoset (P,Q) = RelStr(# (ConFuncs (P,Q)),(ConRelat (P,Q)) #);

definition

let P, Q be non empty strict chain-complete Poset;

let F be non empty Chain of (ConPoset (P,Q));

let p be Element of P;

coherence

{ x where x is Element of Q : ex f being continuous Function of P,Q st

( f in F & x = f . p ) } is non empty Chain of Q;

end;
let F be non empty Chain of (ConPoset (P,Q));

let p be Element of P;

func F -image p -> non empty Chain of Q equals :: POSET_1:def 9

{ x where x is Element of Q : ex f being continuous Function of P,Q st

( f in F & x = f . p ) } ;

correctness { x where x is Element of Q : ex f being continuous Function of P,Q st

( f in F & x = f . p ) } ;

coherence

{ x where x is Element of Q : ex f being continuous Function of P,Q st

( f in F & x = f . p ) } is non empty Chain of Q;

proof end;

:: 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 ) } ;

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 ) } ;

definition

let P, Q be non empty strict chain-complete Poset;

let F be non empty Chain of (ConPoset (P,Q));

ex b_{1} being Function of P,Q st

for p being Element of P

for M being non empty Chain of Q st M = F -image p holds

b_{1} . p = sup M

for b_{1}, b_{2} being Function of P,Q st ( for p being Element of P

for M being non empty Chain of Q st M = F -image p holds

b_{1} . p = sup M ) & ( for p being Element of P

for M being non empty Chain of Q st M = F -image p holds

b_{2} . p = sup M ) holds

b_{1} = b_{2}

end;
let F be non empty Chain of (ConPoset (P,Q));

func sup_func F -> Function of P,Q means :Def10: :: POSET_1:def 10

for p being Element of P

for M being non empty Chain of Q st M = F -image p holds

it . p = sup M;

existence for p being Element of P

for M being non empty Chain of Q st M = F -image p holds

it . p = sup M;

ex b

for p being Element of P

for M being non empty Chain of Q st M = F -image p holds

b

proof end;

uniqueness for b

for M being non empty Chain of Q st M = F -image p holds

b

for M being non empty Chain of Q st M = F -image p holds

b

b

proof end;

:: deftheorem Def10 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 b_{4} being Function of P,Q holds

( b_{4} = sup_func F iff for p being Element of P

for M being non empty Chain of Q st M = F -image p holds

b_{4} . p = sup M );

for P, Q being non empty strict chain-complete Poset

for F being non empty Chain of (ConPoset (P,Q))

for b

( b

for M being non empty Chain of Q st M = F -image p holds

b

Lm17: 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

proof end;

Lm18: 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

proof end;

Lm19: 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

proof end;

Lm20: 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

proof end;

registration

let P, Q be non empty strict chain-complete Poset;

let F be non empty Chain of (ConPoset (P,Q));

correctness

coherence

sup_func F is continuous ;

by Lm20;

end;
let F be non empty Chain of (ConPoset (P,Q));

correctness

coherence

sup_func F is continuous ;

by Lm20;

Lm21: 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))

proof end;

Lm22: 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

proof end;

theorem Th11: :: POSET_1:11

for P, Q being non empty strict chain-complete Poset

for F being non empty Chain of (ConPoset (P,Q)) holds

( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) )

for F being non empty Chain of (ConPoset (P,Q)) holds

( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) )

proof end;

definition
end;

:: 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);

for P, Q being non empty strict chain-complete Poset holds min_func (P,Q) = P --> (Bottom Q);

registration
end;

Lm23: for P, Q being non empty strict chain-complete Poset holds min_func (P,Q) is Element of (ConPoset (P,Q))

proof end;

theorem Th12: :: POSET_1:12

for P, Q being non empty strict chain-complete Poset

for f being Element of (ConPoset (P,Q)) st f = min_func (P,Q) holds

f is_<=_than the carrier of (ConPoset (P,Q))

for f being Element of (ConPoset (P,Q)) st f = min_func (P,Q) holds

f is_<=_than the carrier of (ConPoset (P,Q))

proof end;

registration

let P, Q be non empty strict chain-complete Poset;

coherence

ConPoset (P,Q) is chain-complete

end;
coherence

ConPoset (P,Q) is chain-complete

proof end;

Lm24: 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

proof end;

Lm25: 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))

proof end;

definition

let P be non empty strict chain-complete Poset;

ex b_{1} 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

b_{1} . g = least_fix_point h

for b_{1}, b_{2} 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

b_{1} . 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

b_{2} . g = least_fix_point h ) holds

b_{1} = b_{2}

end;
func fix_func P -> Function of (ConPoset (P,P)),P means :Def12: :: POSET_1:def 12

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 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;

ex b

for g being Element of (ConPoset (P,P))

for h being continuous Function of P,P st g = h holds

b

proof end;

uniqueness for b

for h being continuous Function of P,P st g = h holds

b

for h being continuous Function of P,P st g = h holds

b

b

proof end;

:: deftheorem Def12 defines fix_func POSET_1:def 12 :

for P being non empty strict chain-complete Poset

for b_{2} being Function of (ConPoset (P,P)),P holds

( b_{2} = fix_func P iff for g being Element of (ConPoset (P,P))

for h being continuous Function of P,P st g = h holds

b_{2} . g = least_fix_point h );

for P being non empty strict chain-complete Poset

for b

( b

for h being continuous Function of P,P st g = h holds

b

Lm26: 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 ) )

proof end;

Lm27: for P being non empty strict chain-complete Poset holds fix_func P is monotone Function of (ConPoset (P,P)),P

proof end;

Lm28: 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) )

proof end;

Lm29: 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

proof end;

Lm30: 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

proof end;

Lm31: 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

proof end;

Lm32: 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

proof end;

Lm33: 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

proof end;

Lm34: 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

proof end;

Lm35: 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)) )

proof end;

Lm36: 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)

proof end;

registration
end;