:: Fix-point Theorem for Continuous Functions on Chain-complete Posets
:: by Kazuhisa Ishida and Yasunari Shidama
::
:: Received November 10, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies POSET_1, ORDERS_1, RELAT_1, RELAT_2, XBOOLE_0, FUNCT_1, FUNCT_2,
ORDINAL2, FUNCOP_1, SEQM_3, LATTICES, LATTICE3, YELLOW_0, WAYBEL_0,
ABIAN, TARSKI, CARD_1, FUNCT_7, NAT_1, SUBSET_1, ORDERS_2, XXREAL_0,
STRUCT_0, ARYTM_3, TREES_2, EQREL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, ORDERS_1,
RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, ORDERS_2, ORDERS_3, ORDINAL1,
NUMBERS, FUNCT_7, XXREAL_0, XCMPLX_0, YELLOW_2, LATTICE3, YELLOW_0,
WAYBEL_0, ABIAN;
constructors ORDERS_3, NAT_1, DOMAIN_1, ABIAN, LATTICE3, YELLOW_2, RELSET_1,
NUMBERS;
registrations XBOOLE_0, ORDINAL1, FUNCT_1, PARTFUN1, STRUCT_0, ORDERS_2,
XREAL_0, NAT_1, WAYBEL10, YELLOW_0, WAYBEL24, RELSET_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0;
expansions LATTICE3;
theorems RELSET_1, RELAT_2, ORDERS_2, TARSKI, FUNCT_1, FUNCT_2, XBOOLE_0,
ORDERS_1, ORDERS_3, FUNCOP_1, FUNCT_7, NAT_1, YELLOW_0, ABIAN, YELLOW_2,
WAYBEL_0;
schemes NAT_1, RELSET_1, FUNCT_2;
begin
registration let P be non empty Poset; :: move to ORDERS_2
cluster non empty for Chain of P;
existence
proof
ex L being Chain of P st L is non empty
proof
set z = the Element of P;
set IT={z};
reconsider IT as Chain of P by ORDERS_2:8;
IT is non empty;
hence thesis;
end;
hence thesis;
end;
end;
definition let IT be RelStr;
attr IT is chain-complete means :Def1:
IT is lower-bounded &
for L being Chain of IT st L is non empty holds ex_sup_of L,IT;
end;
theorem Th1:
for P1, P2 being non empty Poset, K being non empty Chain of P1,
h being monotone Function of P1, P2 holds
h.:K is non empty Chain of P2
proof
let P1, P2 be non empty Poset,
K be non empty Chain of P1,
h be monotone Function of P1, P2;
set R = the InternalRel of P2;
set K2 = h.:K;
for x, y be object
st x in K2 & y in K2 & x <>y holds [x,y] in R or [y,x] in R
proof
let x, y be object;
assume A1:x in K2 & y in K2 & x <>y;
then reconsider x,y as Element of P2;
consider a be object such that
A2: a in dom h & a in K & x = h.a
by A1,FUNCT_1:def 6;
consider b be object such that
A3: b in dom h & b in K & y = h.b
by A1,FUNCT_1:def 6;
reconsider a,b as Element of P1 by A2,A3;
a<=b or b<=a by A2,A3,ORDERS_2:11;
then x<=y or y<=x by A2,A3,ORDERS_3:def 5;
hence thesis by ORDERS_2:def 5;
end;
then A4:R is_connected_in K2 by RELAT_2:def 6;
for x be object st x in K2 holds [x,x] in R
proof
let x be object;
assume x in K2;
then reconsider x as Element of P2;
x<=x;
hence thesis by ORDERS_2:def 5;
end;
then R is_reflexive_in K2 by RELAT_2:def 1;
then R is_strongly_connected_in K2 by A4,ORDERS_1:7;
then reconsider K2 as Chain of P2 by ORDERS_2:def 7;
consider a be object such that A5:a in K by XBOOLE_0:7;
a in the carrier of P1 by A5;
then a in dom h by FUNCT_2:def 1;
then h.a in K2 by A5,FUNCT_1:def 6;
hence thesis;
end;
registration
cluster strict chain-complete non empty for Poset;
existence
proof
set z = the set;
set A = {z};
reconsider R = id A as Relation of A;
reconsider R as Order of A;
take IT = RelStr(#A,R#);
reconsider z as Element of IT by TARSKI:def 1;
for L being Chain of IT st L is non empty holds ex_sup_of L,IT
proof
let L be Chain of IT;
assume L is non empty;
for x being Element of IT st x in L holds x <= z by TARSKI:def 1;
then A1: L is_<=_than z;
for y being Element of IT holds
L is_<=_than y implies z <= y by TARSKI:def 1;
hence thesis by A1,YELLOW_0:15;
end;
hence thesis;
end;
end;
registration
cluster chain-complete -> lower-bounded for RelStr;
coherence;
end;
reserve n,m,k for Nat;
reserve x,y,z,X for set;
reserve P,Q for strict chain-complete non empty Poset;
reserve L for non empty Chain of P;
reserve M for non empty Chain of Q;
reserve p,p1,p2,p3,p4 for Element of P;
reserve q,q1,q2 for Element of Q;
reserve f for monotone Function of P,Q;
reserve g,g1,g2 for monotone Function of P,P;
:: Minimum and sup.
theorem Th2:
sup (f.:L) <= f.(sup L)
proof
reconsider M=f.:L as non empty Chain of Q by Th1;
set r = sup L;
set u = f.(sup L);
A1:ex_sup_of L,P & ex_sup_of M,Q by Def1;
for q st q in M holds q <= u
proof
let q;
assume q in M;
then consider x being object such that
A2: x in dom f & x in L & q = f.x by FUNCT_1:def 6;
reconsider x as Element of P by A2;
L is_<=_than r by A1,YELLOW_0:def 9;
then x <= r by A2;
hence thesis by A2,ORDERS_3:def 5;
end;
then M is_<=_than u;
hence thesis by A1,YELLOW_0:def 9;
end;
begin
:: 2. Fix-point theorem for continuous function on chain-complete Poset
:: Primaries--Iteration of monotone functions
Lm1:
for P be non empty Poset, g be monotone Function of P, P,
p be Element of P holds
iter(g,0).p=p
proof
let P be non empty Poset,
g be monotone Function of P, P,
p be Element of P;
set X = the carrier of P;
iter(g,0).p = (id X).p by FUNCT_7:84
.= p;
hence thesis;
end;
definition let P be non empty Poset,
g be monotone Function of P, P,
p be Element of P;
func iterSet(g,p) -> non empty set equals
{x where x is Element of P : ex n being Nat st x = iter(g,n).p};
correctness
proof
set IT = {x where x is Element of P
: ex n being Nat st x = iter(g,n).p};
IT is non empty
proof
iter(g,0).p = p by Lm1;
then p in IT;
hence thesis;
end;
hence thesis;
end;
end;
Lm2:
(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:
p<=p3 & p1=iter(g,n).p & p4= iter(g,n).p3 implies p1 <= p4
proof
defpred U[Nat] means
for p,p3,p1,p4 holds
p<=p3 & p1=iter(g,$1).p & p4= iter(g,$1).p3 implies p1 <= p4;
A1:U[0]
proof
let p,p3,p1,p4;
assume p<=p3 & p1=iter(g,0).p & p4= iter(g,0).p3;
then p<=p3 & p1=p & p4=p3 by Lm1;
hence thesis;
end;
A2: U[k] implies U[k+1]
proof
assume
A3: for p,p3,p1,p4 holds
p<=p3 & p1=iter(g,k).p & p4= iter(g,k).p3 implies p1 <= p4;
U[k+1]
proof
let p,p3,p1,p4;
assume A4:p<=p3 & p1=iter(g,k+1).p & p4= iter(g,k+1).p3;
reconsider x1=iter(g,k).p as Element of P;
reconsider y1=iter(g,k).p3 as Element of P;
A5:x1<=y1 by A4,A3;
iter(g,k+1) = g*iter(g,k) by FUNCT_7:71;
then p1 = g.(iter(g,k).p) & p4 = g.(iter(g,k).p3) by Lm2,A4;
hence thesis by A5,ORDERS_3:def 5;
end;
hence thesis;
end;
U[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Lm4:
p3= g.p & p<=p3 & p1=iter(g,n).p & p4= iter(g,n+k).p implies p1 <= p4
proof
defpred U[Nat] means
for p,p3,p1,p4 holds
p3= g.p & p<=p3 & p1=iter(g,n).p & p4= iter(g,n+$1).p implies p1 <= p4;
A1:U[0];
A2:for k be Nat st U[k] holds U[k+1]
proof
let k;
assume
A3: for p,p3,p1,p4 holds
p3= g.p & p<=p3 & p1=iter(g,n).p & p4= iter(g,n+k).p
implies p1 <= p4;
U[k+1]
proof
let p,p3,p1,p4;
assume A4:p3= g.p & p<=p3 & p1=iter(g,n).p & p4= iter(g,n+(k+1)).p;
reconsider y1=iter(g,n+k).p as Element of P;
A5:p1<=y1 by A4,A3;
iter(g,n+(k+1)) = iter(g,(n+k)+1).=iter(g,n+k)*g by FUNCT_7:69;
then p4 = iter(g,n+k).p3 by Lm2,A4;
then y1<=p4 by A4,Lm3;
hence thesis by A5,ORDERS_2:3;
end;
hence thesis;
end;
for k being Nat holds U[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Lm5:
n<=m & p3 = g.p & p<=p3 & p1=iter(g,n).p & p4 = iter(g,m).p implies p1 <= p4
proof
assume A1:n<=m & p3= g.p & p<=p3 & p1=iter(g,n).p & p4 = iter(g,m).p;
then consider k such that A2:m=n+k by NAT_1:10;
thus thesis by A1,A2,Lm4;
end;
Lm6:
p is_a_fixpoint_of g implies iter(g,n).p = p
proof
defpred U[Nat] means
for p holds p is_a_fixpoint_of g implies iter(g,$1).p = p;
A1:U[0] by Lm1;
A2:for k be Nat st U[k] holds U[k+1]
proof
let k;
assume A3:U[k];
U[k+1]
proof
let p;
assume A4:p is_a_fixpoint_of g;
iter(g,k+1) = g*iter(g,k) by FUNCT_7:71;
then iter(g,k+1).p = g.(iter(g,k).p) by Lm2
.= g.p by A4,A3
.= p by A4,ABIAN:def 3;
hence thesis;
end;
hence thesis;
end;
for k being Nat holds U[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Lm7:
g1 <= g2 & p1 = iter(g1,n).p & p2 = iter(g2,n).p implies p1 <= p2
proof
defpred U[Nat] means
for p,p1,p2 holds
g1 <= g2 & p1 = iter(g1,$1).p & p2 = iter(g2,$1).p
implies p1 <= p2;
A1:U[0]
proof
let p,p1,p2;
assume g1 <= g2 & p1 = iter(g1,0).p & p2 = iter(g2,0).p;
then p1 = p & p2 = p by Lm1;
hence thesis;
end;
A2:for k be Nat st U[k] holds U[k+1]
proof
let k;
assume A3:U[k];
U[k+1]
proof
let p,p1,p2;
assume A4:g1 <= g2 & p1 = iter(g1,k+1).p & p2 = iter(g2,k+1).p;
reconsider q1 = iter(g1,k).p as Element of P;
reconsider q2 = iter(g2,k).p as Element of P;
set r = g1.q2;
A5: q1 <= q2 by A4,A3;
iter(g1,k+1) = g1*iter(g1,k) by FUNCT_7:71;
then A6: p1 = g1.q1 by Lm2,A4;
iter(g2,k+1) = g2*iter(g2,k) by FUNCT_7:71;
then A7: p2 = g2.q2 by Lm2,A4;
A8: p1 <= r by A5,A6,ORDERS_3:def 5;
r <= p2 by A4,A7,YELLOW_2:9;
hence thesis by A8,ORDERS_2:3;
end;
hence thesis;
end;
for k being Nat holds U[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem Th3:
iterSet(g,Bottom P) is non empty Chain of P
proof
set a = Bottom P;
set R = the InternalRel of P;
set L=iterSet(g,a);
A1:x in L implies x is Element of P
proof
assume x in L;
then consider y being Element of P such that
A2: x=y & ex n being Nat st y = iter(g,n).a;
thus thesis by A2;
end;
for x being object holds x in L implies x in the carrier of P
proof let x be object;
assume x in L;
then x is Element of the carrier of P by A1;
hence thesis;
end;
then reconsider L as Subset of P by TARSKI:def 3;
for x,y being object
holds x in L & y in L & x <>y implies [x,y] in R or [y,x] in R
proof let x,y be object;
assume A3:x in L & y in L & x <>y;
then reconsider x,y as Element of P;
consider p such that A4: x=p & ex n st p = iter(g,n).a by A3;
consider p1 such that A5: y=p1 & ex m st p1 = iter(g,m).a by A3;
consider n such that A6:p = iter(g,n).a by A4;
consider m such that A7:p1 = iter(g,m).a by A5;
p<=p1 or p1<=p
proof
set a1 = iter(g,1).a;
A8:a1=g.a by FUNCT_7:70;
per cases;
suppose n<=m;
hence thesis by A6,A7,A8,Lm5,YELLOW_0:44;
end;
suppose m<=n;
hence thesis by A6,A7,A8,Lm5,YELLOW_0:44;
end;
end;
hence thesis by A4,A5,ORDERS_2:def 5;
end;
then A9:R is_connected_in L by RELAT_2:def 6;
for x being object holds x in L implies [x,x] in R
proof let x be object;
assume x in L;
then reconsider x as Element of P;
x<=x;
hence thesis by ORDERS_2:def 5;
end;
then R is_reflexive_in L by RELAT_2:def 1;
then R is_strongly_connected_in L by A9,ORDERS_1:7;
then reconsider L as Chain of P by ORDERS_2:def 7;
L is non empty Chain of P;
hence thesis;
end;
definition let P; let g be monotone Function of P,P;
func iter_min(g) -> non empty Chain of P equals
iterSet(g,Bottom P);
correctness by Th3;
end;
theorem Th4:
sup iter_min(g) = sup (g.:iter_min(g))
proof
reconsider L=g.:iter_min(g) as non empty Chain of P by Th1;
A1:ex_sup_of iter_min(g),P & ex_sup_of L,P by Def1;
set a = Bottom P;
set s1=sup iter_min(g);
set s2=sup L;
A2:iter_min(g) is_<=_than s1 by A1,YELLOW_0:def 9;
A3:L is_<=_than s2 by A1,YELLOW_0:def 9;
for x being Element of P st x in iter_min(g) holds x <= s2
proof
let x be Element of P;
assume x in iter_min(g);
then consider p such that A4:x=p & ex n st p = iter(g,n).a;
consider n such that A5:p=iter(g,n).a by A4;
A6:1<=n implies p in L
proof
assume 1<=n;
then consider k such that A7:n=1+k by NAT_1:10;
reconsider z=iter(g,k).a as Element of P;
z in the carrier of P; then
A8: z in dom g & z in iter_min(g) by FUNCT_2:def 1;
p = (g*iter(g,k)).a by A5,A7,FUNCT_7:71
.= g.z by Lm2;
hence thesis by A8,FUNCT_1:def 6;
end;
n=0 implies p=a by A5,Lm1;
hence thesis by A6,A4,A3,NAT_1:14,YELLOW_0:44;
end;
then iter_min(g) is_<=_than s2;
then A9:s1<=s2 by A1,YELLOW_0:30;
for x being Element of P st x in L holds x <= s1
proof
let x be Element of P;
assume x in L;
then consider z being object such that
A10: z in dom g & z in iter_min(g) & x = g.z by FUNCT_1:def 6;
consider z1 be Element of P such that
A11:z=z1 & ex n st z1 = iter(g,n).a by A10;
consider n such that A12:z1=iter(g,n).a by A11;
set n1=n+1;
g.z = (g*iter(g,n)).a by Lm2,A11,A12
.= iter(g,n1).a by FUNCT_7:71;
then x in iterSet(g,a) by A10;
hence thesis by A2;
end;
then L is_<=_than s1;
then s2<=s1 by A1,YELLOW_0:def 9;
hence thesis by A9,ORDERS_2:2;
end;
theorem Th5:
g1 <= g2 implies sup iter_min(g1) <= sup iter_min(g2)
proof
assume A1:g1 <= g2;
set p2 = sup iter_min(g2);
set a = Bottom P;
A2:ex_sup_of iter_min(g1),P & ex_sup_of iter_min(g2),P by Def1;
then A3:iter_min(g2) is_<=_than p2 by YELLOW_0:def 9;
for x being Element of P st x in iter_min(g1) holds x <= p2
proof
let x be Element of P;
assume x in iter_min(g1);
then consider p such that A4:x=p & ex n st p = iter(g1,n).a;
consider n such that A5:p=iter(g1,n).a by A4;
reconsider y = iter(g2,n).a as Element of P;
y in iter_min(g2);
then A6:y <= p2 by A3;
p <= y by A1,A5,Lm7;
hence thesis by A4,A6,ORDERS_2:3;
end;
then iter_min(g1) is_<=_than p2;
hence thesis by A2,YELLOW_0:30;
end;
:: Continuous function on chain-complete Poset
definition let P,Q be non empty Poset;
let f be Function of P,Q;
attr f is continuous means
f is monotone & for L be non empty Chain of P holds f preserves_sup_of L;
end;
theorem Th6:
for f being Function of P,Q holds f is continuous iff
(f is monotone & for L holds f.(sup L) = sup (f.:L))
proof
let f be Function of P,Q;
thus f is continuous implies
(f is monotone & for L holds f.(sup L) = sup (f.:L))
proof
assume A1:f is continuous;
for L holds f.(sup L) = sup (f.:L)
proof
let L;
A2:f preserves_sup_of L by A1;
ex_sup_of L,P by Def1;
hence thesis by A2,WAYBEL_0:def 31;
end;
hence thesis by A1;
end;
assume that A3:f is monotone and
A4: for L holds f.(sup L) = sup (f.:L);
for L holds f preserves_sup_of L
proof
let L;
reconsider M = f.:L as non empty Chain of Q by A3,Th1;
ex_sup_of M,Q & f.(sup L) = sup M by Def1,A4;
hence thesis by WAYBEL_0:def 31;
end;
hence thesis by A3;
end;
theorem Th7:
for z being Element of Q holds (P-->z) is continuous
proof
let z be Element of Q;
set IT = P --> z;
for L holds IT.(sup L) = sup (IT.:L)
proof
let L;
set M = IT.:L;
for x being Element of Q st x in M holds x <= z
proof
let x be Element of Q;
assume x in M;
then consider a be object such that
A1: a in dom IT & a in L & x = IT.a by FUNCT_1:def 6;
thus thesis by A1,FUNCOP_1:7;
end;
then A2:M is_<=_than z;
for y being Element of Q st M is_<=_than y holds z <= y
proof
let y be Element of Q;
assume A3:M is_<=_than y;
consider a be object such that A4:a in L by XBOOLE_0:def 1;
a in the carrier of P by A4;
then A5:a in dom IT by FUNCOP_1:13;
IT.a = z by A4,FUNCOP_1:7;
then z in M by A4,A5,FUNCT_1:def 6;
hence thesis by A3;
end;
then z = "\/"(M,Q) by A2,YELLOW_0:30;
hence thesis by FUNCOP_1:7;
end;
hence thesis by Th6;
end;
registration let P,Q;
cluster continuous for Function of P, Q;
existence
proof
set z = the Element of Q;
take P-->z;
thus thesis by Th7;
end;
end;
registration let P,Q;
cluster continuous -> monotone for Function of P, Q;
correctness;
end;
theorem Th8:
for f being monotone Function of P,Q holds
(for L holds f.(sup L) <= sup (f.:L)) implies f is continuous
proof
let f be monotone Function of P,Q;
assume A1:for L holds f.(sup L) <= sup (f.:L);
for L holds f.(sup L) = sup (f.:L)
proof
let L;
set a1=f.(sup L);
set a2=sup (f.:L);
A2:a2<=a1 by Th2;
a1<=a2 by A1;
hence thesis by A2,ORDERS_2:2;
end;
hence thesis by Th6;
end;
:: Fix-point theorem for continuous function on chain-complete Poset
Lm8:
g is continuous & p=sup iter_min(g) implies p is_a_fixpoint_of g
proof
A1:dom g = the carrier of P by FUNCT_2:def 1;
reconsider L=g.:iter_min(g) as non empty Chain of P by Th1;
assume A2:g is continuous & p=sup iter_min(g);
then g.p = sup L by Th6
.= p by A2,Th4;
hence thesis by A1,ABIAN:def 3;
end;
Lm9:
p4=sup iter_min(g) implies for p st p is_a_fixpoint_of g holds p4 <= p
proof
assume A1:p4=sup iter_min(g);
for p st p is_a_fixpoint_of g holds p4 <= p
proof
let p;
assume A2:p is_a_fixpoint_of g;
set M = iter_min(g);
set a = Bottom P;
A3:ex_sup_of M,P by Def1;
for p1 st p1 in M holds p1 <= p
proof
let p1;
assume p1 in M;
then consider p2 such that A4:p1=p2 & ex n st p2 = iter(g,n).a;
consider n such that A5:p1=iter(g,n).a by A4;
reconsider q = iter(g,n).p as Element of P;
p1 <= q by A5,Lm3,YELLOW_0:44;
hence thesis by A2,Lm6;
end;
then M is_<=_than p;
hence thesis by A3,A1,YELLOW_0:def 9;
end;
hence thesis;
end;
definition let P; let g be monotone Function of P,P;
assume A1:g is continuous;
func least_fix_point(g) -> Element of P means :Def5:
it is_a_fixpoint_of g & for p st p is_a_fixpoint_of g holds it <= p;
existence
proof
set IT = sup iter_min(g);
take IT;
thus thesis by A1,Lm8,Lm9;
end;
uniqueness
proof
let p1,p2;
assume (p1 is_a_fixpoint_of g &
for p st p is_a_fixpoint_of g holds p1 <= p) &
(p2 is_a_fixpoint_of g &
for p st p is_a_fixpoint_of g holds p2 <= p);
then p1 <= p2 & p2 <= p1;
hence thesis by ORDERS_2:2;
end;
end;
theorem Th9:
for g being continuous Function of P,P holds
least_fix_point(g) = sup iter_min(g)
proof
let g be continuous Function of P,P;
set p = sup iter_min(g);
set q = least_fix_point(g);
p is_a_fixpoint_of g by Lm8;
then A1:q <= p by Def5;
q is_a_fixpoint_of g by Def5;
then p <= q by Lm9;
hence thesis by A1,ORDERS_2:2;
end;
theorem Th10:
for g1,g2 being continuous Function of P,P st g1 <= g2 holds
least_fix_point(g1) <= least_fix_point(g2)
proof
let g1,g2 be continuous Function of P,P;
assume A1: g1 <= g2;
set p1 = sup iter_min(g1);
set p2 = sup iter_min(g2);
p1 = least_fix_point(g1) & p2 = least_fix_point(g2) by Th9;
hence thesis by A1,Th5;
end;
begin
:: 3. Function space of continuous functions on chain-complete Posets
definition let P,Q;
func ConFuncs (P,Q) -> non empty set equals
{x where x is Element of Funcs(the carrier of P,the carrier of Q)
:ex f be continuous Function of P,Q st f=x };
correctness
proof
set IT = {x where x is Element of Funcs(the carrier of P,the carrier of Q)
:ex f be continuous Function of P,Q st f=x };
IT is non empty
proof
set z = the Element of Q;
reconsider f = P-->z as continuous Function of P,Q by Th7;
f is Element of Funcs(the carrier of P,the carrier of Q) by FUNCT_2:8;
then f in IT;
hence thesis;
end;
hence thesis;
end;
end;
Lm10:
for f be Function of P,Q holds f <= f
proof
let f be Function of P,Q;
for p holds f.p <= f.p;
hence thesis by YELLOW_2:9;
end;
Lm11:
for f,g,h be Function of P,Q st f <= g & g <= h holds f <= h
proof
let f,g,h be Function of P,Q;
assume A1:f <= g & g <= h;
for p holds f.p <= h.p
proof
let p;
q=f.p & q2=h.p implies q<=q2
proof
assume A2:q=f.p & q2=h.p;
set q1=g.p;
q<=q1 & q1<=q2 by A2,A1,YELLOW_2:9;
hence thesis by ORDERS_2:3;
end;
hence thesis;
end;
hence thesis by YELLOW_2:9;
end;
Lm12:
for f,g be Function of P,Q st f <= g & g <= f holds f=g
proof
let f,g be Function of P,Q;
assume A1:f <= g & g <= f;
for x being object st x in the carrier of P holds f.x =g.x
proof
let x be object;
assume x in the carrier of P;
then reconsider p=x as Element of P;
set q1=f.p;
set q2=g.p;
A2:q1<=q2 by A1,YELLOW_2:9;
q2<=q1 by A1,YELLOW_2:9;
hence thesis by A2,ORDERS_2:2;
end;
hence thesis by FUNCT_2:12;
end;
definition let P,Q;
func ConRelat(P,Q) -> Relation of ConFuncs(P,Q) means :Def7:
for x,y 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
proof
defpred U[object,object] means ex f,g being Function of P,Q st
$1=f & $2=g & f <= g;
set X = ConFuncs(P,Q);
consider IT being Relation of X,X such that
A1:for x,y being object holds [x,y] in IT iff x in X & y in X & U[x,y]
from RELSET_1:sch 1;
take IT;
thus thesis by A1;
end;
uniqueness
proof
set X = ConFuncs(P,Q);
let Y1,Y2 be Relation of X;
defpred P1[set,set] means
$1 in X & $2 in X
& ex f,g being Function of P,Q st
$1=f & $2=g & f <= g;
(for x,y holds ([x,y] in Y1 iff P1[x,y]) &
for x,y holds ([x,y] in Y2 iff P1[x,y]) )
implies Y1=Y2
proof
assume A2:for x,y holds ([x,y] in Y1 iff P1[x,y]) &
for x,y holds ([x,y] in Y2 iff P1[x,y]);
then A3:for x1 being Element of X, y1 being Element of X
holds ([x1,y1] in Y1 iff P1[x1,y1] );
A4:for x being Element of X, y being Element of X
holds [x,y] in Y2 iff P1[x,y] by A2;
thus thesis from RELSET_1:sch 4(A3,A4);
end;
hence thesis;
end;
end;
Lm13:
field ConRelat(P,Q) c= ConFuncs(P,Q)
proof
ConFuncs(P,Q) \/ ConFuncs(P,Q) c= ConFuncs(P,Q);
hence thesis by RELSET_1:8;
end;
Lm14:
ConRelat(P,Q) is_reflexive_in ConFuncs(P,Q)
proof
set R = ConRelat(P,Q);
for x being object holds x in ConFuncs(P,Q) implies [x,x] in R
proof let x be object;
assume A1:x in ConFuncs(P,Q);
then consider x1 be Element of Funcs(the carrier of P,the carrier of Q)
such that
A2:x=x1 and A3: ex f be continuous Function of P,Q st f=x1;
consider f be continuous Function of P,Q such that A4:f=x1 by A3;
f <= f by Lm10;
hence thesis by A1,A2,A4,Def7;
end;
hence thesis by RELAT_2:def 1;
end;
Lm15:
ConRelat(P,Q) is_transitive_in ConFuncs(P,Q)
proof
set X = ConFuncs(P,Q);
set R = ConRelat(P,Q);
for x,y,z being object holds
x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R
proof let x,y,z be object;
assume A1:x in X & y in X & z in X & [x,y] in R & [y,z] in R;
then consider f,g being Function of P,Q such that
A2:x=f & y=g & f <= g by Def7;
consider g1,h being Function of P,Q such that
A3:y=g1 & z=h & g1 <= h by A1,Def7;
f <= h by A3,A2,Lm11;
hence thesis by A1,A2,A3,Def7;
end;
hence thesis by RELAT_2:def 8;
end;
Lm16:
ConRelat(P,Q) is_antisymmetric_in ConFuncs(P,Q)
proof
set X = ConFuncs(P,Q);
reconsider R = ConRelat(P,Q) as Relation of ConFuncs(P,Q);
for x,y being object holds
x in X & y in X & [x,y] in R & [y,x] in R implies x = y
proof let x,y be object;
assume A1:x in X & y in X & [x,y] in R & [y,x] in R;
then consider f,g being Function of P,Q such that
A2:x=f & y=g & f <= g by Def7;
consider g1,f1 being Function of P,Q such that
A3:y=g1 & x=f1 & g1 <= f1 by A1,Def7;
thus thesis by A2,A3,Lm12;
end;
hence thesis by RELAT_2:def 4;
end;
registration let P,Q;
cluster ConRelat(P,Q) -> reflexive;
coherence
proof
ConRelat(P,Q) is_reflexive_in field ConRelat(P,Q)
proof
reconsider R = ConRelat(P,Q) as Relation of ConFuncs(P,Q);
for x being object holds
x in field R implies [x,x] in R
proof let x be object;
assume A1:x in field R;
A2:field R c= ConFuncs(P,Q) by Lm13;
R is_reflexive_in ConFuncs(P,Q) by Lm14;
hence thesis by A1,A2,RELAT_2:def 1;
end;
hence thesis by RELAT_2:def 1;
end;
hence thesis by RELAT_2:def 9;
end;
cluster ConRelat(P,Q) -> transitive;
coherence
proof
ConRelat(P,Q) is_transitive_in field ConRelat(P,Q)
proof
set X = field ConRelat(P,Q);
set R = ConRelat(P,Q);
for x,y,z being object holds
x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R
proof let x,y,z be object;
assume A3:x in X & y in X & z in X & [x,y] in R & [y,z] in R;
set X1=ConFuncs(P,Q);
A4:field R c= X1 by Lm13;
R is_transitive_in X1 by Lm15;
hence thesis by A3,A4,RELAT_2:def 8;
end;
hence thesis by RELAT_2:def 8;
end;
hence thesis by RELAT_2:def 16;
end;
cluster ConRelat(P,Q) -> antisymmetric;
coherence
proof
ConRelat(P,Q) is_antisymmetric_in field ConRelat(P,Q)
proof
set X = field ConRelat(P,Q);
reconsider R = ConRelat(P,Q) as Relation of ConFuncs(P,Q);
for x,y being object holds
x in X & y in X & [x,y] in R & [y,x] in R implies x = y
proof let x,y be object;
assume A5:x in X & y in X & [x,y] in R & [y,x] in R;
set X1=ConFuncs(P,Q);
A6:field R c= X1 by Lm13;
R is_antisymmetric_in X1 by Lm16;
hence thesis by A5,A6,RELAT_2:def 4;
end;
hence thesis by RELAT_2:def 4;
end;
hence thesis by RELAT_2:def 12;
end;
end;
definition let P,Q;
func ConPoset(P,Q) -> strict non empty Poset equals
RelStr(#ConFuncs(P,Q),ConRelat(P,Q)#);
correctness
by Lm14,Lm15,Lm16,ORDERS_2:def 2,ORDERS_2:def 3,ORDERS_2:def 4;
end;
reserve F for non empty Chain of ConPoset(P,Q);
definition let P,Q,F,p;
func F-image p -> non empty Chain of Q equals
{x where x is Element of Q
:ex f being continuous Function of P,Q st f in F & x=f.p};
correctness
proof
set R = the InternalRel of Q;
set IT = {x where x is Element of Q
:ex f being continuous Function of P,Q st f in F & x=f.p};
for x being object holds x in IT implies x in the carrier of Q
proof let x be object;
assume x in IT;
then consider a being Element of Q such that
A1:x=a & ex f being continuous Function of P,Q st f in F & a=f.p;
reconsider x as Element of the carrier of Q by A1;
x in the carrier of Q;
hence thesis;
end;
then reconsider IT as Subset of Q by TARSKI:def 3;
for x,y being object holds
x in IT & y in IT & x <>y implies [x,y] in R or [y,x] in R
proof let x,y be object;
assume A2:x in IT & y in IT & x <>y;
then consider a being Element of Q such that
A3: x=a & ex f being continuous Function of P,Q st f in F & a=f.p;
consider f being continuous Function of P,Q such that
A4: f in F & a=f.p by A3;
consider b being Element of Q such that
A5: y=b & ex g being continuous Function of P,Q st g in F & b=g.p by A2;
consider g being continuous Function of P,Q such that
A6: g in F & b=g.p by A5;
set S =the InternalRel of ConPoset(P,Q);
A7:S is_strongly_connected_in F by ORDERS_2:def 7;
per cases by A7,A4,A6,RELAT_2:def 7;
suppose [f,g] in S;
then consider f1,g1 being Function of P,Q such that
A8:f=f1 & g=g1 & f1 <= g1 by Def7;
a <= b by A8,A4,A6,YELLOW_2:9;
hence thesis by A3,A5,ORDERS_2:def 5;
end;
suppose [g,f] in S;
then consider g1,f1 being Function of P,Q such that
A9:g=g1 & f=f1 & g1 <= f1 by Def7;
b<= a by A9,A4,A6,YELLOW_2:9;
hence thesis by A3,A5,ORDERS_2:def 5;
end;
end;
then A10:R is_connected_in IT by RELAT_2:def 6;
for x being object holds
x in IT implies [x,x] in R
proof let x be object;
assume x in IT;
then reconsider x as Element of Q;
x<=x;
hence thesis by ORDERS_2:def 5;
end;
then R is_reflexive_in IT by RELAT_2:def 1;
then R is_strongly_connected_in IT by A10,ORDERS_1:7;
then reconsider IT as Chain of Q by ORDERS_2:def 7;
consider a be object such that A11:a in F by XBOOLE_0:7;
a in ConFuncs(P,Q) by A11; then
consider b being Element of Funcs(the carrier of P,the carrier of Q)
such that
A12: a=b & ex f be continuous Function of P,Q st f=b;
consider f be continuous Function of P,Q such that A13:f=b by A12;
reconsider c = f.p as Element of Q;
c in IT by A11,A12,A13;
hence thesis;
end;
end;
definition let P,Q,F;
func sup_func(F) -> Function of P,Q means :Def10:
for p,M holds M=F-image p implies it.p=sup M;
existence
proof
set X = the carrier of P;
set Y = the carrier of Q;
defpred U[object,object] means for p,M holds p= $1 & M=F-image p
implies $2=sup M;
A1:for x being object st x in X ex y being object st y in Y & U[x,y]
proof
let x be object;
assume x in X;
then reconsider x as Element of P;
reconsider a = F-image x as non empty Chain of Q;
set y = sup a;
take y;
thus thesis;
end;
consider IT being Function of X,Y such that
A2: for x being object st x in X holds U[x,IT.x] from FUNCT_2:sch 1(A1);
for p,M holds M=F-image p implies IT.p=sup M by A2;
hence thesis;
end;
uniqueness
proof
let f,g be Function of P,Q;
(for p,M holds M=F-image p implies f.p=sup M) &
(for p,M holds M=F-image p implies g.p=sup M) implies f=g
proof
assume A3:(for p,M holds M=F-image p implies f.p=sup M) &
(for p,M holds M=F-image p implies g.p=sup M);
set X = the carrier of P;
for x being object st x in X holds f.x = g.x
proof
let x be object;
assume x in X;
then reconsider p= x as Element of P;
reconsider M = F-image p as non empty Chain of Q;
f.x = sup M by A3 .= g.x by A3;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
hence thesis;
end;
end;
Lm17:
sup_func(F) is monotone
proof
reconsider f=sup_func(F) as Function of P,Q;
for p,p1 st p <= p1 for q,q1 st q = f.p & q1 = f.p1 holds q <= q1
proof
let p,p1;
assume A1:p <= p1;
for q,q1 st q = f.p & q1 = f.p1 holds q <= q1
proof
let q,q1;
assume A2:q = f.p & q1 = f.p1;
reconsider X= F-image p as non empty Chain of Q;
reconsider X1= F-image p1 as non empty Chain of Q;
A3:ex_sup_of X,Q & ex_sup_of X1,Q by Def1;
A4:q=sup X by A2,Def10;
q1=sup X1 by A2,Def10;
then A5:X1 is_<=_than q1 by A3,YELLOW_0:def 9;
for x being Element of Q st x in X holds x <= q1
proof
let x be Element of Q;
assume x in X;
then consider a being Element of Q such that
A6:x=a & ex g being continuous Function of P,Q st g in F & a=g.p;
consider g being continuous Function of P,Q such that
A7: g in F & a=g.p by A6;
reconsider b=g.p1 as Element of Q;
A8:a <= b by A1,A7,ORDERS_3:def 5;
b in X1 by A7;
then b <= q1 by A5;
hence thesis by A6,A8,ORDERS_2:3;
end;
then X is_<=_than q1;
hence thesis by A3,A4,YELLOW_0:def 9;
end;
hence thesis;
end;
hence thesis by ORDERS_3:def 5;
end;
Lm18:
q in M implies q <= sup M
proof
assume A1:q in M;
A2:ex_sup_of M,Q by Def1;
set x = sup M;
M is_<=_than x by A2,YELLOW_0:def 9;
hence thesis by A1;
end;
Lm19:
(for q st q in M holds q<=q1) implies sup M <= q1
proof
assume for q st q in M holds q<=q1;
then A1:M is_<=_than q1;
A2:ex_sup_of M,Q by Def1;
thus thesis by A2,A1,YELLOW_0:def 9;
end;
Lm20:
sup_func(F) is continuous
proof
reconsider f=sup_func(F) as monotone Function of P,Q by Lm17;
for L holds f.(sup L) <= sup (f.:L)
proof
let L;
reconsider M1 = f.:L as non empty Chain of Q by Th1;
set q1 = sup M1;
set a = sup L;
set M = F-image a;
A1:f.a = sup M by Def10;
for q st q in M holds q <=q1
proof
let q;
assume q in M;
then consider q0 be Element of Q such that
A2:q=q0 & ex g being continuous Function of P,Q st g in F & q0=g.a;
consider g being continuous Function of P,Q such that
A3: g in F & q0=g.a by A2;
reconsider M2=g.:L as non empty Chain of Q by Th1;
A4:q = sup M2 by Th6,A2,A3;
for q2 st q2 in M2 holds q2 <= q1
proof
let q2;
assume q2 in M2;
then consider x being object such that
A5: x in dom g & x in L & q2 = g.x
by FUNCT_1:def 6;
reconsider x as Element of P by A5;
set Mx=F-image x;
A6:f.x= sup Mx by Def10;
set y = f.x;
x in the carrier of P;
then x in dom f by FUNCT_2:def 1;
then y in M1 by A5,FUNCT_1:def 6;
then A7:y <= q1 by Lm18;
q2 in F-image x by A5,A3;
then q2 <= sup Mx by Lm18;
hence thesis by A7,A6,ORDERS_2:3;
end;
hence thesis by A4,Lm19;
end;
hence thesis by A1,Lm19;
end;
hence thesis by Th8;
end;
registration let P,Q,F;
cluster sup_func(F) -> continuous;
correctness by Lm20;
end;
Lm21:
sup_func(F) is Element of ConPoset(P,Q)
proof
set x = sup_func(F);
A1: x is Element of Funcs(the carrier of P,the carrier of Q) by FUNCT_2:8;
reconsider x = sup_func(F) as continuous Function of P,Q;
x in ConFuncs(P,Q) by A1;
hence thesis;
end;
Lm22:
for x st x in F holds ex g being continuous Function of P,Q st x=g
proof
let x;
assume x in F;
then x in ConFuncs(P,Q);
then consider y be Element of Funcs(the carrier of P,the carrier of Q)
such that A1:x = y & ex g be continuous Function of P,Q st g=y;
thus thesis by A1;
end;
theorem Th11:
ex_sup_of F, ConPoset(P,Q) & sup_func(F) = "\/"(F,ConPoset(P,Q))
proof
set X = ConPoset(P,Q);
set f1 = sup_func(F);
reconsider f=f1 as Element of ConPoset(P,Q) by Lm21;
for x being Element of X st x in F holds x <= f
proof
let x be Element of X;
assume A1:x in F;
then consider g1 being continuous Function of P,Q such that
A2: x = g1 by Lm22;
reconsider g = g1 as Element of X by A2;
for p holds g1.p <= f1.p
proof
let p;
q1=g1.p & q2=f1.p implies q1<=q2
proof
assume A3:q1=g1.p & q2=f1.p;
then A4:q1 in F-image p by A1,A2;
reconsider M = F-image p as non empty Chain of Q;
q2 = sup M by Def10,A3;
hence thesis by A4,Lm18;
end;
hence thesis;
end;
then g1 <= f1 by YELLOW_2:9;
then [g,f] in ConRelat(P,Q) by Def7;
hence thesis by A2,ORDERS_2:def 5;
end;
then A5:F is_<=_than f;
for y being Element of X holds F is_<=_than y implies f <= y
proof
let y be Element of X;
y in ConFuncs(P,Q);
then consider y1 being Element of Funcs(the carrier of P,the carrier of Q)
such that A6:y = y1 & ex gy be continuous Function of P,Q st gy =y1;
consider gy being continuous Function of P,Q
such that A7:gy = y1 by A6;
F is_<=_than y implies f <= y
proof
assume A8:F is_<=_than y;
for p holds f1.p <= gy.p
proof
let p;
q1=f1.p & q2=gy.p implies q1<=q2
proof
assume A9:q1=f1.p & q2=gy.p;
reconsider M=F-image p as non empty Chain of Q;
for q st q in M holds q<=q2
proof
let q;
assume q in M;
then consider a being Element of Q such that
A10:q=a & ex g being continuous Function of P,Q st g in F & a=g.p;
consider g be continuous Function of P,Q such that
A11: g in F & a=g.p by A10;
reconsider g1 = g as Element of ConPoset(P,Q) by A11;
g1 <= y by A8,A11;
then [g1,y] in ConRelat(P,Q) by ORDERS_2:def 5;
then consider g2,g3 being Function of P,Q such that
A12:g1=g2 & y=g3 & g2 <= g3 by Def7;
thus thesis by A12,A6,A7,A10,A11,A9,YELLOW_2:9;
end;
then sup M <= q2 by Lm19;
hence thesis by A9,Def10;
end;
hence thesis;
end;
then f1 <= gy by YELLOW_2:9;
then [f,y] in ConRelat(P,Q) by A6,A7,Def7;
hence thesis by ORDERS_2:def 5;
end;
hence thesis;
end;
hence thesis by A5,YELLOW_0:30;
end;
definition let P,Q;
func min_func(P,Q) -> Function of P,Q equals
P --> Bottom Q;
coherence;
end;
registration let P,Q;
cluster min_func(P,Q) -> continuous;
coherence by Th7;
end;
Lm23:
min_func(P,Q) is Element of ConPoset(P,Q)
proof
reconsider f = min_func(P,Q) as continuous Function of P,Q;
reconsider x = f as Element of Funcs(the carrier of P,the carrier of Q)
by FUNCT_2:8;
x in ConFuncs(P,Q);
hence thesis;
end;
theorem Th12:
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
let f be Element of ConPoset(P,Q);
assume A1:f = min_func(P,Q);
set f1 = min_func(P,Q);
for x being Element of ConPoset(P,Q) holds f<=x
proof
let x be Element of ConPoset(P,Q);
x in ConFuncs(P,Q);
then consider x1 being Element of Funcs(the carrier of P,the carrier of Q)
such that
A2: x = x1 & ex g be continuous Function of P,Q st g=x1;
consider g being continuous Function of P,Q such that
A3: g=x1 by A2;
for p holds f1.p <= g.p
proof
let p;
q1=f1.p & q2=g.p implies q1<=q2
proof
assume q1=f1.p & q2=g.p;
then q1=Bottom Q by FUNCOP_1:7;
hence thesis by YELLOW_0:44;
end;
hence thesis;
end;
then f1 <= g by YELLOW_2:9;
then [f,x] in ConRelat(P,Q) by A2,A3,Def7,A1;
hence thesis by ORDERS_2:def 5;
end;
hence thesis;
end;
registration let P,Q;
cluster ConPoset(P,Q) -> chain-complete;
coherence
proof
set IT = ConPoset(P,Q);
ex a being Element of IT st a is_<=_than the carrier of IT
proof
reconsider a = min_func(P,Q) as Element of ConPoset(P,Q)
by Lm23;
take a;
thus thesis by Th12;
end; then
A1: IT is lower-bounded by YELLOW_0:def 4;
for L being Chain of IT st L is non empty holds ex_sup_of L,IT
by Th11;
hence thesis by A1;
end;
end;
begin
:: 4. Continuity of fix-point function from ConPoset(P,P) to P
Lm24:
x is Element of ConPoset(P,P) implies x is continuous Function of P,P
proof
assume x is Element of ConPoset(P,P);
then x in ConFuncs(P,P);
then consider y be Element of Funcs(the carrier of P,the carrier of P)
such that A1:x = y & ex g be continuous Function of P,P st g=y;
thus thesis by A1;
end;
Lm25:
g is continuous Function of P,P implies g is Element of ConPoset(P,P)
proof
assume A1:g is continuous Function of P,P;
reconsider g1 = g as Element of Funcs(the carrier of P,the carrier of P)
by FUNCT_2:8;
g1 in ConFuncs (P,P) by A1;
hence thesis;
end;
definition let P;
func fix_func(P) -> Function of ConPoset(P,P), P means :Def12:
for g being Element of ConPoset(P,P),
h being continuous Function of P, P st g = h holds
it.g = least_fix_point h;
existence
proof
set X = the carrier of ConPoset(P,P);
set Y = the carrier of P;
defpred U[object,object] means
for g being Element of ConPoset(P,P),
h being continuous Function of P, P st
g = h & g = $1 holds $2 = least_fix_point h;
A1: for x being object st x in X ex y being object st y in Y & U[x,y]
proof
let x be object;
assume x in X;
then reconsider x as Element of ConPoset(P,P);
reconsider h = x as continuous Function of P, P by Lm24;
take least_fix_point h;
thus thesis;
end;
consider IT being Function of X,Y such that
A2: for x being object st x in X holds U[x,IT.x] from FUNCT_2:sch 1(A1);
for g being Element of ConPoset(P,P),
h being continuous Function of P, P st g = h holds
IT.g = least_fix_point h by A2;
hence thesis;
end;
uniqueness
proof
let h1,h2 be Function of ConPoset(P,P),P such that
A3: (for g being Element of ConPoset(P,P),
h being continuous Function of P, P st g = h holds
h1.g = least_fix_point h) &
(for g being Element of ConPoset(P,P),
h being continuous Function of P, P st g = h holds
h2.g = least_fix_point h);
set X = the carrier of ConPoset(P,P);
for x being object st x in X holds h1.x = h2.x
proof
let x be object;
assume x in X;
then reconsider g = x as Element of ConPoset(P,P);
reconsider h = g as continuous Function of P, P by Lm24;
h1.x = least_fix_point h by A3
.= h2.x by A3;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
Lm26:
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
let p1,p2 be Element of ConPoset(P,P);
assume p1 <= p2;
then A1:[p1,p2] in ConRelat(P,P) by ORDERS_2:def 5;
ex g1,g2 being continuous Function of P,P st p1=g1 & p2=g2 & g1 <= g2
proof
consider g1,g2 being Function of P,P such that
A2: p1=g1 & p2=g2 & g1 <= g2 by A1,Def7;
reconsider h1 = p1, h2 = p2 as continuous Function of P, P
by Lm24;
g1 = h1 by A2;
then reconsider g1 as continuous Function of P, P;
g2 = h2 by A2;
then reconsider g2 as continuous Function of P, P;
take g1,g2;
thus thesis by A2;
end;
hence thesis;
end;
Lm27:
fix_func(P) is monotone Function of ConPoset(P,P),P
proof
set IT = fix_func(P);
for p1,p2 being Element of ConPoset(P,P) st p1 <= p2
for a,b being Element of P
st a = IT.p1 & b = IT.p2 holds a <= b
proof
let p1,p2 be Element of ConPoset(P,P);
assume A1:p1 <= p2;
let a, b be Element of P;
assume A2:a = IT.p1 & b = IT.p2;
consider g1,g2 being continuous Function of P,P such that
A3: p1=g1 & p2=g2 & g1 <= g2 by A1,Lm26;
a = least_fix_point(g1) & b = least_fix_point(g2) by A2,Def12,A3;
hence thesis by A3,Th10;
end;
hence thesis by ORDERS_3:def 5;
end;
Lm28:
for G being non empty Chain of ConPoset(P,P),n,X,x
st X = {p where p is Element of P
: ex g being Element of ConPoset(P,P),
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,
g being continuous Function of P,P
st x=p & g in G & p = iter(g,n).(Bottom P)
proof
let G be non empty Chain of ConPoset(P,P);
let n,X,x;
assume X = {p where p is Element of P : ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,n).(Bottom P)}
& x in X;
then consider p be Element of P such that
A1:x=p & ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,n).(Bottom P);
thus thesis by A1;
end;
Lm29:
for G being non empty Chain of ConPoset(P,P) ,n, X
st X = {p where p is Element of P
: ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,n).(Bottom P)}
holds x in X implies x is Element of P
proof
let G be non empty Chain of ConPoset(P,P);
let n,X;
assume A1:X = {p where p is Element of P
: ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,n).(Bottom P)};
x in X implies x is Element of P
proof
assume x in X;
then consider p being Element of P such that
A2: x=p & ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,n).(Bottom P) by A1;
thus thesis by A2;
end;
hence thesis;
end;
Lm30:
for G being non empty Chain of ConPoset(P,P), n, X
st X = {p where p is Element of P
: ex g being Element of ConPoset(P,P),
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
let G be non empty Chain of ConPoset(P,P);
let n,X;
assume A1:X = {p where p is Element of P
: ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,n).(Bottom P)};
consider g be object such that A2:g in G by XBOOLE_0:def 1;
reconsider g as Element of ConPoset(P,P) by A2;
reconsider gg = g as continuous Function of P,P by Lm24;
reconsider p = iter(gg,n).(Bottom P) as Element of P;
A3:p in X by A1,A2;
for x being object holds x in X implies x in the carrier of P
proof let x be object;
assume x in X;
then x is Element of the carrier of P by Lm29,A1;
hence thesis;
end;
hence thesis by A3,TARSKI:def 3;
end;
Lm31:
for G being non empty Chain of ConPoset(P,P),
f,g being monotone Function of P,P st f in G & g in G
holds f <= g or g <= f
proof
let G be non empty Chain of ConPoset(P,P);
let f,g be monotone Function of P,P;
assume A1: f in G & g in G;
set S = the InternalRel of ConPoset(P,P);
A2:S is_strongly_connected_in G by ORDERS_2:def 7;
per cases by A2,A1,RELAT_2:def 7;
suppose [f,g] in S;
then consider f1,g1 being Function of P,P such that
A3:f=f1 & g=g1 & f1 <= g1 by Def7;
thus thesis by A3;
end;
suppose [g,f] in S;
then consider g1,f1 being Function of P,P such that
A4:g=g1 & f=f1 & g1 <= f1 by Def7;
thus thesis by A4;
end;
end;
Lm32:
for G being non empty Chain of ConPoset(P,P) ,n, X
st X = {p where p is Element of P
: ex g being Element of ConPoset(P,P),
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
let G be non empty Chain of ConPoset(P,P);
let n,X;
assume A1: X = {p where p is Element of P
: ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,n).(Bottom P)};
set R = the InternalRel of P;
reconsider X as non empty Subset of P by A1,Lm30;
for x,y being object holds
x in X & y in X & x <>y implies [x,y] in R or [y,x] in R
proof let x,y be object;
assume A2:x in X & y in X & x <>y;
then consider p1 being Element of P,
g1 being continuous Function of P,P such that
A3: x=p1 & g1 in G & p1 = iter(g1,n).(Bottom P) by A1,Lm28;
consider p2 being Element of P,
g2 being continuous Function of P,P such that
A4: y=p2 & g2 in G & p2 = iter(g2,n).(Bottom P) by A1,A2,Lm28;
per cases by A3,A4,Lm31;
suppose g1 <= g2;
then p1 <= p2 by Lm7,A3,A4;
hence thesis by A3,A4,ORDERS_2:def 5;
end;
suppose g2 <= g1;
then p2 <= p1 by Lm7,A3,A4;
hence thesis by A3,A4,ORDERS_2:def 5;
end;
end;
then A5:R is_connected_in X by RELAT_2:def 6;
for x being object holds
x in X implies [x,x] in R
proof let x be object;
assume x in X;
then reconsider x as Element of P;
x<=x;
hence thesis by ORDERS_2:def 5;
end;
then R is_reflexive_in X by RELAT_2:def 1;
then R is_strongly_connected_in X by A5,ORDERS_1:7;
hence thesis by ORDERS_2:def 7;
end;
Lm33:
for h being Function of ConPoset(P,P),P,
G being non empty Chain of ConPoset(P,P),x
holds x in G implies h.x in h.:G
proof
let h be Function of ConPoset(P,P),P;
let G be non empty Chain of ConPoset(P,P);
let x;
assume A1:x in G;
set X = the carrier of ConPoset(P,P);
set Y = the carrier of P;
reconsider h as Function of X,Y;
x in X by A1; then
x in dom h by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:def 6;
end;
Lm34:
for g being continuous Function of P,P ,p,p1,n
holds p = (fix_func(P)).g & p1 = (iter(g,n)).(Bottom P)
implies p1 <= p
proof
let g be continuous Function of P,P;
let p,p1,n;
set a = Bottom P;
assume A1: p = (fix_func(P)).g & p1 = (iter(g,n)).a;
then A2:p1 in iterSet(g,a);
reconsider g1 = g as Element of ConPoset(P,P) by Lm25;
reconsider G1 = g1 as continuous Function of P,P;
p = least_fix_point(G1) by Def12,A1
.= sup iter_min(g) by Th9;
hence thesis by Lm18,A2;
end;
Lm35:
for G being non empty Chain of ConPoset(P,P), x being set, n being Nat,
M being non empty Chain of P,
g1 being monotone Function of P,P
st M = {p where p is Element of P
: ex g being Element of ConPoset(P,P),
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
let G be non empty Chain of ConPoset(P,P);
let x be set;
let n be Nat;
let M be non empty Chain of P;
let g1 be monotone Function of P,P;
assume A1:M = {p where p is Element of P
: ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,n).(Bottom P)}
& x in g1.:M;
then ex y being object st y in dom g1 & y in M & x = g1.y
by FUNCT_1:def 6;
then consider y being Element of M such that
A2:y in M & x = g1.y;
consider p being Element of P such that
A3:y = p & ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,n).(Bottom P) by A1,A2;
thus thesis by A2,A3;
end;
Lm36:
for G being non empty Chain of ConPoset(P,P)
holds (fix_func(P)).(sup G) <= sup ((fix_func(P)).:G)
proof
let G be non empty Chain of ConPoset(P,P);
reconsider h = fix_func(P) as monotone Function of ConPoset(P,P),P
by Lm27;
h.(sup G) <= sup (h.:G)
proof
reconsider L = h.:G as non empty Chain of P by Th1;
set g0 = sup G;
set p0 = h.g0;
reconsider G0 = g0 as continuous Function of P,P by Lm24;
A1:p0 = least_fix_point(G0) by Def12;
A2:sup G = sup_func(G) by Th11;
then reconsider g0 as continuous Function of P,P;
set a = Bottom P;
reconsider I0 = iterSet(g0,a) as non empty Chain of P by Th3;
A3: p0 = sup iter_min(g0) by Th9,A1
.= sup I0;
A4:ex_sup_of I0,P by Def1;
for x being Element of P st x in I0 holds x <= sup L
proof
let x be Element of P;
assume x in I0;
then consider y being Element of P such that
A5: x=y & ex n being Nat st y = iter(g0,n).a;
consider n0 being Nat such that A6:x = iter(g0,n0).a by A5;
set M0 = {p where p is Element of P
: ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,n0).a};
reconsider M0 as non empty Chain of P by Lm32;
for p st p in M0 holds p <= sup L
proof
let p;
assume p in M0;
then consider p0 being Element of P,
g being continuous Function of P,P such that
A7: p=p0 & g in G & p0 = iter(g,n0).a by Lm28;
set r = h.g;
r in L by A7,Lm33;
then reconsider r as Element of P;
A8:r <= sup L by Lm18,A7,Lm33;
p <= r by A7,Lm34;
hence thesis by A8,ORDERS_2:3;
end; then
A9: sup M0 <= sup L by Lm19;
defpred U[Nat] means
for z being Element of P,M being non empty Chain of P
st z = iter(g0,$1).a &
M = {p where p is Element of P
:ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,$1).a}
holds z <= sup M;
A10:U[0]
proof
let z be Element of P;
let M be non empty Chain of P;
assume z = iter(g0,0).a;
then z = a by Lm1;
hence thesis by YELLOW_0:44;
end;
A11: U[k] implies U[k+1]
proof
assume A12:U[k];
for z1 being Element of P,M1 being non empty Chain of P
st z1 = iter(g0,k+1).a &
M1 = {p where p is Element of P
:ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,k+1).a}
holds z1 <= sup M1
proof
let z1 be Element of P;
let M1 be non empty Chain of P;
assume
A13:z1 = iter(g0,k+1).a & M1 = {p where p is Element of P
:ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,k+1).a};
reconsider z = iter(g0,k).a as Element of P;
A14:z1 = (g0*iter(g0,k)).a by A13,FUNCT_7:71
.= g0.z by Lm2;
reconsider M = {p where p is Element of P
:ex g being Element of ConPoset(P,P),
h being continuous Function of P,P
st h = g & g in G & p = iter(h,k).a}
as non empty Chain of P by Lm32;
reconsider M0 = g0.:M as non empty Chain of P by Th1;
A15:g0.(sup M) = sup M0 by Th6;
A16:ex_sup_of M0,P by Def1;
for q being Element of P st q in M0 holds q <= sup M1
proof
let q be Element of P;
assume q in M0;
then consider g being continuous Function of P,P such that
A17: g in G & q = g0.(iter(g,k).a) by Lm35;
reconsider a1 = iter(g,k).a as Element of P;
reconsider W = G-image a1 as non empty Chain of P;
A18:q = sup W by A17,Def10,A2;
A19:ex_sup_of W,P by Def1;
for q1 being Element of P st q1 in W holds q1 <= sup M1
proof
let q1 be Element of P;
assume q1 in W;
then consider q2 being Element of P such that
A20:q1 = q2 & ex g1 being continuous Function of P,P
st g1 in G & q2=g1.a1;
consider g1 be continuous Function of P,P
such that A21:g1 in G & q1=g1.a1 by A20;
per cases by A17,A21,Lm31;
suppose g1 <= g;
then A22:q1 <= g.a1 by A21,YELLOW_2:9;
set a2 = g.a1;
reconsider g2 = g as Element of ConPoset(P,P)
by Lm25;
reconsider gg = g2 as continuous Function of P,P;
a2 = (g*iter(g,k)).a by Lm2
.= iter(gg,k+1).a by FUNCT_7:71;
then a2 in M1 by A13,A17;
then a2 <= sup M1 by Lm18;
hence thesis by A22,ORDERS_2:3;
end;
suppose A23:g <= g1;
reconsider a2 = iter(g1,k).a as Element of P;
a1 <= a2 by A23,Lm7;
then A24:q1 <= g1.a2 by A21,ORDERS_3:def 5;
set a3 = g1.a2;
reconsider g2 = g1 as Element of ConPoset(P,P)
by Lm25;
reconsider gg = g2 as continuous Function of P,P;
a3 = (g1*iter(g1,k)).a by Lm2
.= iter(gg,k+1).a by FUNCT_7:71;
then a3 in M1 by A13,A21;
then a3 <= sup M1 by Lm18;
hence thesis by A24,ORDERS_2:3;
end;
end;
then W is_<=_than sup M1;
hence thesis by A18,A19,YELLOW_0:def 9;
end;
then M0 is_<=_than sup M1;
then A25:sup M0 <= sup M1 by A16,YELLOW_0:def 9;
z <= sup M by A12;
then z1 <= sup M0 by A14,A15,ORDERS_3:def 5;
hence thesis by A25,ORDERS_2:3;
end;
hence thesis;
end;
U[k] from NAT_1:sch 2(A10,A11);
then x <= sup M0 by A6;
hence thesis by A9,ORDERS_2:3;
end;
then I0 is_<=_than sup L;
hence thesis by A3,A4,YELLOW_0:def 9;
end;
hence thesis;
end;
registration let P;
cluster fix_func(P) -> continuous;
coherence
proof
reconsider f = fix_func(P) as monotone Function of ConPoset(P,P),P
by Lm27;
for L be non empty Chain of ConPoset(P,P)
holds f.(sup L) <= sup (f.:L) by Lm36;
hence thesis by Th8;
end;
end;