:: Fix-point Theorem for Continuous Functions on Chain-complete Posets
:: by Kazuhisa Ishida and Yasunari Shidama
::
:: Received November 10, 2009
:: Copyright (c) 2009 Association of Mizar Users
environ
vocabularies POSET_1, ORDERS_1, RELAT_1, RELAT_2, XBOOLE_0, FUNCT_1, FUNCT_2,
ORDINAL2, FUNCOP_1, NUMBERS, 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, DOMAIN_1, FUNCT_2, BINOP_1, FUNCOP_1, STRUCT_0,
ORDERS_2, ORDERS_3, NUMBERS, NAT_1, FUNCT_3, FUNCT_7, XXREAL_0, XCMPLX_0,
LATTICES, YELLOW_2, LATTICE3, YELLOW_0, WAYBEL_0, ABIAN;
constructors RELAT_2, PARTFUN1, ORDERS_2, ORDERS_3, FUNCOP_1, FUNCT_3,
BINOP_1, FUNCT_4, NAT_1, REAL_1, DOMAIN_1, XXREAL_0, XCMPLX_0, XREAL_0,
ABIAN, LATTICE3, YELLOW_0, YELLOW_2, RELSET_1;
registrations XBOOLE_0, ORDINAL1, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, FRAENKEL, STRUCT_0, ORDERS_2, ORDERS_3, FUNCOP_1, XREAL_0,
NAT_1, NUMBERS, REAL_1, XXREAL_0, RELAT_1, WAYBEL10, ORDERS_1, LATTICE3,
YELLOW_0, ABIAN, WAYBEL_0, WAYBEL24;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCOP_1, XBOOLE_0, YELLOW_0, ABIAN, LATTICE3, STRUCT_0,
FUNCT_2;
theorems RELAT_1, RELSET_1, RELAT_2, ORDERS_2, TARSKI, ZFMISC_1, FUNCT_1,
FUNCT_2, XBOOLE_0, XBOOLE_1, ORDERS_1, ORDERS_3, FUNCOP_1, FUNCT_7,
NAT_1, LATTICE3, YELLOW_0, ABIAN, YELLOW_2, WAYBEL_0;
schemes NAT_1, RELSET_1, FUNCT_2;
begin
:: 1. Monotone function, chain and chain-complete Poset
Lemiter01: for f being Function st rng f c= dom f holds
iter (f,0) = id(dom f)
proof
let f be Function;
assume rng f c= dom f;
then dom f \/ rng f = dom f by XBOOLE_1:12;
hence thesis by FUNCT_7:70;
end;
Lemiter02: for f being Function, n be Nat st
rng f c= dom f holds dom iter(f,n) = dom f & rng iter(f,n) c= dom f
proof
let f be Function, n be Nat;
defpred U[Nat] means
dom iter(f,$1) = dom f & rng iter(f,$1) c= dom f;
assume rng f c= dom f;
then iter(f,0) = id dom f by Lemiter01;
then
A1: U[ 0] by RELAT_1:71;
A2: for k be Nat holds U[k] implies U[k+1]
proof
let k be Nat;
assume
A3: dom iter(f,k) = dom f & rng iter(f,k) c= dom f;
iter(f,k+1) = f*iter(f,k) & iter(f,k+1) = iter(f,k)*f
by FUNCT_7:71,FUNCT_7:73;
then dom iter(f,k+1) = dom iter(f,k) &
rng iter(f,k+1) c= rng iter(f,k) by A3,RELAT_1:45,46;
hence thesis by A3,XBOOLE_1:1;
end;
for k be Nat holds U[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Lemiter03:
for X be set, f being Function of X,X, n be Nat holds
iter(f,n) is Function of X,X
proof
let X be set, f be Function of X,X, n be Nat;
A1: X = {} implies X = {}; then
A2: dom f = X & rng f c= X by FUNCT_2:def 1;
then dom iter(f,n) = X & rng iter(f,n) c= X by Lemiter02;
then reconsider R = iter(f,n) as Relation of X,X by RELSET_1:11;
dom R = X & rng R c= X by A2,Lemiter02;
hence thesis by A1,FUNCT_2:def 1;
end;
registration let P be non empty Poset; :: move to ORDERS_2
cluster non empty Chain of P;
existence
proof
ex L being Chain of P st L is non empty
proof
consider z being Element of P;
set IT={z};
reconsider IT as Chain of P by ORDERS_2:35;
IT is non empty;
hence thesis;
end;
hence thesis;
end;
end;
LemMin01:
for A being non empty RelStr, a being Element of A holds
a is_<=_than the carrier of A iff for x being Element of A holds a <= x
proof
let A be non empty RelStr, a be Element of A;
(for x being Element of A holds a <= x) implies
a is_<=_than the carrier of A
proof
assume A2:for x being Element of A holds a <= x;
a is_<=_than the carrier of A
proof
let x be Element of A;
thus thesis by A2;
end;
hence thesis;
end;
hence thesis by LATTICE3:def 8;
end;
definition let IT be RelStr;
attr IT is chain-complete means :DefchainComplete:
IT is lower-bounded &
for L being Chain of IT st L is non empty holds ex_sup_of L,IT;
end;
theorem ThChain1:
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 set st
x in K2 & y in K2 & x <>y holds [x,y] in R or [y,x] in R
proof
let x, y be set;
assume B1:x in K2 & y in K2 & x <>y;
then reconsider x,y as Element of P2;
consider a be set such that B2: a in dom h & a in K & x = h.a
by B1,FUNCT_1:def 12;
consider b be set such that B3: b in dom h & b in K & y = h.b
by B1,FUNCT_1:def 12;
reconsider a,b as Element of P1 by B2,B3;
a<=b or b<=a by ORDERS_2:38,B2,B3;
then x<=y or y<=x by ORDERS_3:def 5,B2,B3;
hence thesis by ORDERS_2:def 9;
end;
then A1:R is_connected_in K2 by RELAT_2:def 6;
for x be set st x in K2 holds [x,x] in R
proof
let x be set;
assume x in K2;
then reconsider x as Element of P2;
x<=x;
hence thesis by ORDERS_2:def 9;
end;
then R is_reflexive_in K2 by RELAT_2:def 1;
then R is_strongly_connected_in K2 by A1,ORDERS_1:92;
then reconsider K2 as Chain of P2 by ORDERS_2:def 11;
consider a be set such that A2:a in K by XBOOLE_0:7;
a in the carrier of P1 by A2;
then a in dom h by FUNCT_2:def 1;
then h.a in K2 by FUNCT_1:def 12,A2;
hence thesis;
end;
registration
cluster strict chain-complete non empty Poset;
existence
proof
consider z be 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
proof
let x be Element of IT such that C1: x in L;
per cases by ZFMISC_1:39;
suppose L = {};
hence thesis by C1;
end;
suppose L = {z};
thus thesis by TARSKI:def 1;
end;
end;
then B2: L is_<=_than z by LATTICE3:def 9;
for y being Element of IT holds
L is_<=_than y implies z <= y by TARSKI:def 1;
hence thesis by B2,YELLOW_0:15;
end;
hence thesis by DefchainComplete;
end;
end;
registration
cluster chain-complete -> lower-bounded RelStr;
coherence by DefchainComplete;
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 Thmonotone02:
sup (f.:L) <= f.(sup L)
proof
reconsider M=f.:L as non empty Chain of Q by ThChain1;
set t = sup M;
set r = sup L;
set u = f.(sup L);
A01:ex_sup_of L,P & ex_sup_of M,Q by DefchainComplete;
for q st q in M holds q <= u
proof
let q;
assume q in M;
then consider x such that
B1: x in dom f & x in L & q = f.x by FUNCT_1:def 12;
reconsider x as Element of P by B1;
L is_<=_than r by A01,YELLOW_0:def 9;
then x <= r by B1,LATTICE3:def 9;
hence thesis by ORDERS_3:def 5,B1;
end;
then M is_<=_than u by LATTICE3:def 9;
hence thesis by A01,YELLOW_0:def 9;
end;
begin
:: 2. Fix-point theorem for continuous function on chain-complete Poset
:: Primaries--Iteration of monotone functions
Lemiter10:
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:86
.= p by FUNCT_1:35;
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 Lemiter10;
then p in IT;
hence thesis;
end;
hence thesis;
end;
end;
Lemiter11:
iter(g,n).p is Element of P
proof
set X = the carrier of P;
reconsider g1 = iter(g,n) as Function of X,X by Lemiter03;
g1.p in X;
hence thesis;
end;
Lemiter12:
(g*iter(g,n)).p = g.(iter(g,n).p) & (iter(g,n)*g).p = iter(g,n).(g.p)
proof
set X = the carrier of P;
reconsider g1 = iter(g,n) as Function of X,X by Lemiter03;
(g*g1).p = g.(g1.p) & (g1*g).p = g1.(g.p) by FUNCT_2:21;
hence thesis;
end;
Lemiter13:
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 Lemiter10;
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 B1:p<=p3 & p1=iter(g,k+1).p & p4= iter(g,k+1).p3;
reconsider x1=iter(g,k).p as Element of P by Lemiter11;
reconsider y1=iter(g,k).p3 as Element of P by Lemiter11;
B2:x1<=y1 by B1,A3;
iter(g,k+1) = g*iter(g,k) by FUNCT_7:73;
then p1 = g.(iter(g,k).p) & p4 = g.(iter(g,k).p3) by Lemiter12,B1;
hence thesis by B2,ORDERS_3:def 5;
end;
hence thesis;
end;
U[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Lemiter14:
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 B1: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 by Lemiter11;
B2:p1<=y1 by B1,A3;
iter(g,n+(k+1)) = iter(g,(n+k)+1).=iter(g,n+k)*g by FUNCT_7:71;
then p4 = iter(g,n+k).p3 by Lemiter12,B1;
then y1<=p4 by B1,Lemiter13;
hence thesis by B2,ORDERS_2:26;
end;
hence thesis;
end;
for k being Nat holds U[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
Lemiter15:
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;
consider k such that A2:m=n+k by A1,NAT_1:10;
thus thesis by A1,A2,Lemiter14;
end;
Lemiter16:
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 Lemiter10;
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 B1:p is_a_fixpoint_of g;
iter(g,k+1) = g*iter(g,k) by FUNCT_7:73;
then iter(g,k+1).p = g.(iter(g,k).p) by Lemiter12
.= g.p by B1,A3
.= p by B1,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;
Lemiter17:
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 Lemiter10;
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 B1:g1 <= g2 & p1 = iter(g1,k+1).p & p2 = iter(g2,k+1).p;
reconsider q1 = iter(g1,k).p as Element of P by Lemiter11;
reconsider q2 = iter(g2,k).p as Element of P by Lemiter11;
set r = g1.q2;
B2: q1 <= q2 by B1,A3;
B03: iter(g1,k+1) = g1*iter(g1,k) by FUNCT_7:73;
B3: p1 = g1.q1 by B03,Lemiter12,B1;
B04: iter(g2,k+1) = g2*iter(g2,k) by FUNCT_7:73;
B4: p2 = g2.q2 by B04,Lemiter12,B1;
B5: p1 <= r by B2,B3,ORDERS_3:def 5;
r <= p2 by YELLOW_2:10,B1,B4;
hence thesis by B5,ORDERS_2:26;
end;
hence thesis;
end;
for k being Nat holds U[k] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem ThiterSet1:
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
B1: x=y & ex n being Nat st y = iter(g,n).a;
thus thesis by B1;
end;
x in L implies x in the carrier of P
proof
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;
x in L & y in L & x <>y implies [x,y] in R or [y,x] in R
proof
assume B1:x in L & y in L & x <>y;
then reconsider x,y as Element of P;
consider p such that B2: x=p & ex n st p = iter(g,n).a by B1;
consider p1 such that B3: y=p1 & ex m st p1 = iter(g,m).a by B1;
consider n such that B4:p = iter(g,n).a by B2;
consider m such that B5:p1 = iter(g,m).a by B3;
p<=p1 or p1<=p
proof
set a1 = iter(g,1).a;
C1:a1=g.a by FUNCT_7:72;
per cases;
suppose n<=m;
hence thesis by B4,B5,C1,YELLOW_0:44,Lemiter15;
end;
suppose m<=n;
hence thesis by B4,B5,C1,YELLOW_0:44,Lemiter15;
end;
end;
hence thesis by ORDERS_2:def 9,B2,B3;
end;
then A1:R is_connected_in L by RELAT_2:def 6;
x in L implies [x,x] in R
proof
assume x in L;
then reconsider x as Element of P;
x<=x;
hence thesis by ORDERS_2:def 9;
end;
then R is_reflexive_in L by RELAT_2:def 1;
then R is_strongly_connected_in L by A1,ORDERS_1:92;
then reconsider L as Chain of P by ORDERS_2:def 11;
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 ThiterSet1;
end;
theorem ThiterSet2:
sup iter_min(g) = sup (g.:iter_min(g))
proof
reconsider L=g.:iter_min(g) as non empty Chain of P by ThChain1;
A00:ex_sup_of iter_min(g),P & ex_sup_of L,P by DefchainComplete;
set a = Bottom P;
set s1=sup iter_min(g);
set s2=sup L;
A201:iter_min(g) is_<=_than s1 by A00,YELLOW_0:def 9;
A301:L is_<=_than s2 by A00,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 B2:x=p & ex n st p = iter(g,n).a;
consider n such that B3:p=iter(g,n).a by B2;
B4:1<=n implies p in L
proof
assume 1<=n;
then consider k such that C1:n=1+k by NAT_1:10;
reconsider z=iter(g,k).a as Element of P by Lemiter11;
z in the carrier of P; then
C2: z in dom g & z in iter_min(g) by FUNCT_2:def 1;
p = (g*iter(g,k)).a by FUNCT_7:73,B3,C1
.= g.z by Lemiter12;
hence thesis by C2,FUNCT_1:def 12;
end;
n=0 implies p=a by B3,Lemiter10;
hence thesis by B4,NAT_1:14,B2,YELLOW_0:44,A301,LATTICE3:def 9;
end;
then iter_min(g) is_<=_than s2 by LATTICE3:def 9;
then A4:s1<=s2 by A00,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 such that
B2: z in dom g & z in iter_min(g) & x = g.z by FUNCT_1:def 12;
consider z1 be Element of P such that
B3:z=z1 & ex n st z1 = iter(g,n).a by B2;
consider n such that B4:z1=iter(g,n).a by B3;
set n1=n+1;
g.z = (g*iter(g,n)).a by Lemiter12,B3,B4
.= iter(g,n1).a by FUNCT_7:73;
then x in iterSet(g,a) by B2;
hence thesis by A201,LATTICE3:def 9;
end;
then L is_<=_than s1 by LATTICE3:def 9;
then s2<=s1 by YELLOW_0:def 9,A00;
hence thesis by A4,ORDERS_2:25;
end;
theorem ThiterSet3:
g1 <= g2 implies sup iter_min(g1) <= sup iter_min(g2)
proof
assume A1:g1 <= g2;
set p1 = sup iter_min(g1), 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 DefchainComplete;
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 B1:x=p & ex n st p = iter(g1,n).a;
consider n such that B2:p=iter(g1,n).a by B1;
reconsider y = iter(g2,n).a as Element of P by Lemiter11;
y in iter_min(g2);
then B3:y <= p2 by LATTICE3:def 9,A3;
p <= y by A1,B2,Lemiter17;
hence thesis by B1,B3,ORDERS_2:26;
end;
then iter_min(g1) is_<=_than p2 by LATTICE3:def 9;
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 :Defcontinuous:
f is monotone & for L be non empty Chain of P holds f preserves_sup_of L;
end;
theorem Thcontinuous01:
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;
B1:f preserves_sup_of L by A1,Defcontinuous;
ex_sup_of L,P by DefchainComplete;
hence thesis by WAYBEL_0:def 31,B1;
end;
hence thesis by A1,Defcontinuous;
end;
assume that B1:f is monotone and
B2: 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 B1,ThChain1;
ex_sup_of M,Q & f.(sup L) = sup M by DefchainComplete,B2;
hence thesis by WAYBEL_0:def 31;
end;
hence thesis by B1,Defcontinuous;
end;
theorem Thcontinuous02:
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 set such that
D1: a in dom IT & a in L & x = IT.a by FUNCT_1:def 12;
thus thesis by D1,FUNCOP_1:13;
end;
then B3:M is_<=_than z by LATTICE3:def 9;
for y being Element of Q st M is_<=_than y holds z <= y
proof
let y be Element of Q;
assume D1:M is_<=_than y;
consider a be set such that D2:a in L by XBOOLE_0:def 1;
a in the carrier of P by D2;
then D3:a in dom IT by FUNCOP_1:19;
IT.a = z by D2,FUNCOP_1:13;
then z in M by D2,D3,FUNCT_1:def 12;
hence thesis by D1,LATTICE3:def 9;
end;
then z = "\/"(M,Q) by B3,YELLOW_0:30;
hence thesis by FUNCOP_1:13;
end;
hence thesis by Thcontinuous01;
end;
registration let P,Q;
cluster continuous Function of P, Q;
existence
proof
consider z being Element of Q;
take P-->z;
thus thesis by Thcontinuous02;
end;
end;
registration let P,Q;
cluster continuous -> monotone Function of P, Q;
correctness by Defcontinuous;
end;
theorem Thcontinuous03:
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 B1: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);
set M = f.:L;
C2:a2<=a1 by Thmonotone02;
a1<=a2 by B1;
hence thesis by ORDERS_2:25,C2;
end;
hence thesis by Thcontinuous01;
end;
:: Fix-point theorem for continuous function on chain-complete Poset
Lemfixpoint01:
g is continuous & p=sup iter_min(g) implies p is_a_fixpoint_of g
proof
A01:dom g = the carrier of P by FUNCT_2:def 1;
reconsider L=g.:iter_min(g) as non empty Chain of P by ThChain1;
assume A1:g is continuous & p=sup iter_min(g);
then g.p = sup L by Thcontinuous01
.= p by A1,ThiterSet2;
hence thesis by A01,ABIAN:def 3;
end;
Lemfixpoint02:
p4=sup iter_min(g) implies for p st p is_a_fixpoint_of g holds p4 <= p
proof
assume A0:p4=sup iter_min(g);
for p st p is_a_fixpoint_of g holds p4 <= p
proof
let p;
assume A1:p is_a_fixpoint_of g;
set M = iter_min(g);
set a = Bottom P;
A2:ex_sup_of M,P by DefchainComplete;
for p1 st p1 in M holds p1 <= p
proof
let p1;
assume p1 in M;
then consider p2 such that B1:p1=p2 & ex n st p2 = iter(g,n).a;
consider n such that B2:p1=iter(g,n).a by B1;
reconsider q = iter(g,n).p as Element of P by Lemiter11;
p1 <= q by B2,YELLOW_0:44,Lemiter13;
hence thesis by A1,Lemiter16;
end;
then M is_<=_than p by LATTICE3:def 9;
hence thesis by A2,YELLOW_0:def 9,A0;
end;
hence thesis;
end;
definition let P; let g be monotone Function of P,P;
assume A0:g is continuous;
func least_fix_point(g) -> Element of P means :Defleastfixpoint:
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 A0,Lemfixpoint01,Lemfixpoint02;
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:25;
end;
end;
theorem Thfixpoint01:
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 Lemfixpoint01;
then A2:q <= p by Defleastfixpoint;
q is_a_fixpoint_of g by Defleastfixpoint;
then p <= q by Lemfixpoint02;
hence thesis by A2,ORDERS_2:25;
end;
theorem Thfixpoint02:
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 Thfixpoint01;
hence thesis by A1,ThiterSet3;
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
consider z being Element of Q;
reconsider f = P-->z as continuous Function of P,Q by Thcontinuous02;
f is Element of Funcs(the carrier of P,the carrier of Q)
by FUNCT_2:11;
then f in IT;
hence thesis;
end;
hence thesis;
end;
end;
Lemlessthan01:
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:10;
end;
Lemlessthan02:
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 C1:q=f.p & q2=h.p;
set q1=g.p;
q<=q1 & q1<=q2 by C1,A1,YELLOW_2:10;
hence thesis by ORDERS_2:26;
end;
hence thesis;
end;
hence thesis by YELLOW_2:10;
end;
Lemlessthan03:
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 st x in the carrier of P holds f.x =g.x
proof
let x;
assume x in the carrier of P;
then reconsider p=x as Element of P;
set q1=f.p;
set q2=g.p;
B1:q1<=q2 by A1,YELLOW_2:10;
q2<=q1 by A1,YELLOW_2:10;
hence thesis by B1,ORDERS_2:25;
end;
hence thesis by FUNCT_2:18;
end;
definition let P,Q;
func ConRelat(P,Q) -> Relation of ConFuncs(P,Q) means :DefConRelat:
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[set,set] 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 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 B1:for x,y holds ([x,y] in Y1 iff P1[x,y]) &
for x,y holds ([x,y] in Y2 iff P1[x,y]);
B2:for x1 being Element of X, y1 being Element of X
holds ([x1,y1] in Y1 iff P1[x1,y1] ) by B1;
B3:for x being Element of X, y being Element of X
holds [x,y] in Y2 iff P1[x,y] by B1;
thus thesis from RELSET_1:sch 4(B2,B3);
end;
hence thesis;
end;
end;
LemConRelat01:
field ConRelat(P,Q) c= ConFuncs(P,Q)
proof
ConFuncs(P,Q) \/ ConFuncs(P,Q) c= ConFuncs(P,Q);
hence thesis by RELSET_1:19;
end;
LemConRelat02:
ConRelat(P,Q) is_reflexive_in ConFuncs(P,Q)
proof
set R = ConRelat(P,Q);
x in ConFuncs(P,Q) implies [x,x] in R
proof
assume B1:x in ConFuncs(P,Q);
then consider x1 be Element of Funcs(the carrier of P,the carrier of Q)
such that
B3:x=x1 and B4: ex f be continuous Function of P,Q st f=x1;
consider f be continuous Function of P,Q such that B5:f=x1 by B4;
f <= f by Lemlessthan01;
hence thesis by B1,B3,B5,DefConRelat;
end;
hence thesis by RELAT_2:def 1;
end;
LemConRelat03:
ConRelat(P,Q) is_transitive_in ConFuncs(P,Q)
proof
set X = ConFuncs(P,Q);
set R = ConRelat(P,Q);
x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R
proof
assume B1:x in X & y in X & z in X & [x,y] in R & [y,z] in R;
consider f,g being Function of P,Q such that
B2:x=f & y=g & f <= g by B1,DefConRelat;
consider g1,h being Function of P,Q such that
B3:y=g1 & z=h & g1 <= h by B1,DefConRelat;
f <= h by B3,B2,Lemlessthan02;
hence thesis by B1,B2,B3,DefConRelat;
end;
hence thesis by RELAT_2:def 8;
end;
LemConRelat04:
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);
x in X & y in X & [x,y] in R & [y,x] in R implies x = y
proof
assume B1:x in X & y in X & [x,y] in R & [y,x] in R;
consider f,g being Function of P,Q such that
B2:x=f & y=g & f <= g by B1,DefConRelat;
consider g1,f1 being Function of P,Q such that
B3:y=g1 & x=f1 & g1 <= f1 by B1,DefConRelat;
thus thesis by B2,B3,Lemlessthan03;
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);
x in field R implies [x,x] in R
proof
assume B0:x in field R;
B1:field R c= ConFuncs(P,Q) by LemConRelat01;
R is_reflexive_in ConFuncs(P,Q) by LemConRelat02;
hence thesis by B0,B1,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);
x in X & y in X & z in X & [x,y] in R & [y,z] in R implies [x,z] in R
proof
assume B0:x in X & y in X & z in X & [x,y] in R & [y,z] in R;
set X1=ConFuncs(P,Q);
B1:field R c= X1 by LemConRelat01;
R is_transitive_in X1 by LemConRelat03;
hence thesis by B0,B1,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);
x in X & y in X & [x,y] in R & [y,x] in R implies x = y
proof
assume B0:x in X & y in X & [x,y] in R & [y,x] in R;
set X1=ConFuncs(P,Q);
B1:field R c= X1 by LemConRelat01;
R is_antisymmetric_in X1 by LemConRelat04;
hence thesis by B0,B1,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
proof
set IT = RelStr(#ConFuncs(P,Q),ConRelat(P,Q)#);
A1: the InternalRel of IT is_reflexive_in the carrier of IT
by LemConRelat02;
A2: the InternalRel of IT is_transitive_in the carrier of IT
by LemConRelat03;
the InternalRel of IT is_antisymmetric_in the carrier of IT
by LemConRelat04;
hence thesis by A1,A2,ORDERS_2:def 4,ORDERS_2:def 5,ORDERS_2:def 6;
end;
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};
x in IT implies x in the carrier of Q
proof
assume x in IT;
then consider a being Element of Q such that
B1: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 B1;
x in the carrier of Q;
hence thesis;
end;
then reconsider IT as Subset of Q by TARSKI:def 3;
x in IT & y in IT & x <>y implies [x,y] in R or [y,x] in R
proof
assume B1:x in IT & y in IT & x <>y;
consider a being Element of Q such that
B2: x=a & ex f being continuous Function of P,Q st f in F & a=f.p by B1;
consider f being continuous Function of P,Q such that
B3: f in F & a=f.p by B2;
consider b being Element of Q such that
B5: y=b & ex g being continuous Function of P,Q st g in F & b=g.p by B1;
consider g being continuous Function of P,Q such that
B6: g in F & b=g.p by B5;
set S =the InternalRel of ConPoset(P,Q);
B9:S is_strongly_connected_in F by ORDERS_2:def 11;
per cases by B9,RELAT_2:def 7,B3,B6;
suppose [f,g] in S;
then consider f1,g1 being Function of P,Q such that
C1:f=f1 & g=g1 & f1 <= g1 by DefConRelat;
a <= b by C1,YELLOW_2:10,B3,B6;
hence thesis by B2,B5,ORDERS_2:def 9;
end;
suppose [g,f] in S;
then consider g1,f1 being Function of P,Q such that
C2:g=g1 & f=f1 & g1 <= f1 by DefConRelat;
b<= a by C2,YELLOW_2:10,B3,B6;
hence thesis by B2,B5,ORDERS_2:def 9;
end;
end;
then A1:R is_connected_in IT by RELAT_2:def 6;
x in IT implies [x,x] in R
proof
assume x in IT;
then reconsider x as Element of Q;
x<=x;
hence thesis by ORDERS_2:def 9;
end;
then R is_reflexive_in IT by RELAT_2:def 1;
then R is_strongly_connected_in IT by A1,ORDERS_1:92;
then reconsider IT as Chain of Q by ORDERS_2:def 11;
consider a be set such that A2:a in F by XBOOLE_0:7;
a in ConFuncs(P,Q) by A2; then
consider b being Element of Funcs(the carrier of P,the carrier of Q)
such that
A3: a=b & ex f be continuous Function of P,Q st f=b;
consider f be continuous Function of P,Q such that A4:f=b by A3;
reconsider c = f.p as Element of Q;
c in IT by A2,A3,A4;
hence thesis;
end;
end;
definition let P,Q,F;
func sup_func(F) -> Function of P,Q means :Defsupfunc:
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[set,set] means for p,M holds p= $1 & M=F-image p
implies $2=sup M;
A1:for x st x in X ex y st y in Y & U[x,y]
proof
let x;
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 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 C1:(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;
set Y = the carrier of Q;
for x st x in X holds f.x = g.x
proof
let x;
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 C1 .= g.x by C1;
hence thesis;
end;
hence thesis by FUNCT_2:18;
end;
hence thesis;
end;
end;
Lemsup01:
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;
A00:ex_sup_of X,Q & ex_sup_of X1,Q by DefchainComplete;
A3:q=sup X by A2,Defsupfunc;
q1=sup X1 by A2,Defsupfunc;
then A4:X1 is_<=_than q1 by A00,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
B2: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
B3: g in F & a=g.p by B2;
reconsider b=g.p1 as Element of Q;
B4:a <= b by A1,B3,ORDERS_3:def 5;
b in X1 by B3;
then b <= q1 by A4,LATTICE3:def 9;
hence thesis by B2,B4,ORDERS_2:26;
end;
then X is_<=_than q1 by LATTICE3:def 9;
hence thesis by A00,A3,YELLOW_0:def 9;
end;
hence thesis;
end;
hence thesis by ORDERS_3:def 5;
end;
Lem201:
q in M implies q <= sup M
proof
assume A1:q in M;
A00:ex_sup_of M,Q by DefchainComplete;
set x = sup M;
M is_<=_than x by YELLOW_0:def 9,A00;
hence thesis by LATTICE3:def 9,A1;
end;
Lem202:
(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 by LATTICE3:def 9;
A00:ex_sup_of M,Q by DefchainComplete;
reconsider x = sup M as Element of Q;
thus thesis by YELLOW_0:def 9,A00,A1;
end;
Lemsup02:
sup_func(F) is continuous
proof
reconsider f=sup_func(F) as monotone Function of P,Q by Lemsup01;
for L holds f.(sup L) <= sup (f.:L)
proof
let L;
reconsider M1 = f.:L as non empty Chain of Q by ThChain1;
set q1 = sup M1;
set a = sup L;
set M = F-image a;
A2:f.a = sup M by Defsupfunc;
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
B1: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
B2: g in F & q0=g.a by B1;
reconsider M2=g.:L as non empty Chain of Q by ThChain1;
B3:q = sup M2 by Thcontinuous01,B1,B2;
for q2 st q2 in M2 holds q2 <= q1
proof
let q2;
assume q2 in M2;
then consider x such that C1: x in dom g & x in L & q2 = g.x
by FUNCT_1:def 12;
reconsider x as Element of P by C1;
set Mx=F-image x;
C2:f.x= sup Mx by Defsupfunc;
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 C1,FUNCT_1:def 12;
then C3:y <= q1 by Lem201;
q2 in F-image x by C1,B2;
then q2 <= sup Mx by Lem201;
hence thesis by C3,ORDERS_2:26,C2;
end;
hence thesis by B3,Lem202;
end;
hence thesis by A2,Lem202;
end;
hence thesis by Thcontinuous03;
end;
registration let P,Q,F;
cluster sup_func(F) -> continuous;
correctness by Lemsup02;
end;
Lemsup03:
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:11;
reconsider x = sup_func(F) as continuous Function of P,Q;
x in ConFuncs(P,Q) by A1;
hence thesis;
end;
Lem301:
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 A2:x = y & ex g be continuous Function of P,Q st g=y;
thus thesis by A2;
end;
theorem ThConPoset01:
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 Lemsup03;
for x being Element of X st x in F holds x <= f
proof
let x be Element of X;
assume B1:x in F;
then consider g1 being continuous Function of P,Q such that
B2: x = g1 by Lem301;
reconsider g = g1 as Element of X by B2;
for p holds g1.p <= f1.p
proof
let p;
q1=g1.p & q2=f1.p implies q1<=q2
proof
assume C1:q1=g1.p & q2=f1.p;
then C2:q1 in F-image p by B1,B2;
reconsider M = F-image p as non empty Chain of Q;
q2 = sup M by Defsupfunc,C1;
hence thesis by C2,Lem201;
end;
hence thesis;
end;
then g1 <= f1 by YELLOW_2:10;
then [g,f] in ConRelat(P,Q) by DefConRelat;
hence thesis by B2,ORDERS_2:def 9;
end;
then A1:F is_<=_than f by LATTICE3:def 9;
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 B01:y = y1 & ex gy be continuous Function of P,Q st gy =y1;
consider gy being continuous Function of P,Q
such that B02:gy = y1 by B01;
F is_<=_than y implies f <= y
proof
assume B1: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 C1: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
D1: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
D2: g in F & a=g.p by D1;
reconsider g1 = g as Element of ConPoset(P,Q) by D2;
g1 <= y by B1,LATTICE3:def 9,D2;
then [g1,y] in ConRelat(P,Q) by ORDERS_2:def 9;
then consider g2,g3 being Function of P,Q such that
D3:g1=g2 & y=g3 & g2 <= g3 by DefConRelat;
thus thesis by D3,B01,B02,D1,D2,C1,YELLOW_2:10;
end;
then sup M <= q2 by Lem202;
hence thesis by C1,Defsupfunc;
end;
hence thesis;
end;
then f1 <= gy by YELLOW_2:10;
then [f,y] in ConRelat(P,Q) by B01,B02,DefConRelat;
hence thesis by ORDERS_2:def 9;
end;
hence thesis;
end;
hence thesis by A1,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 Thcontinuous02;
end;
LemMinFunc01:
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:11;
x in ConFuncs(P,Q);
hence thesis;
end;
theorem ThConPoset02:
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
B1: x = x1 & ex g be continuous Function of P,Q st g=x1;
consider g being continuous Function of P,Q such that
B2: g=x1 by B1;
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:13;
hence thesis by YELLOW_0:44;
end;
hence thesis;
end;
then f1 <= g by YELLOW_2:10;
then [f,x] in ConRelat(P,Q) by B1,B2,DefConRelat,A1;
hence thesis by ORDERS_2:def 9;
end;
hence thesis by LemMin01;
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 LemMinFunc01;
take a;
thus thesis by ThConPoset02;
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 ThConPoset01;
hence thesis by DefchainComplete,A1;
end;
end;
begin
:: 4. Continuity of fix-point function from ConPoset(P,P) to P
LemCastFunc01:
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;
LemCastFunc02:
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:11;
g1 in ConFuncs (P,P) by A1;
hence thesis;
end;
definition let P;
func fix_func(P) -> Function of ConPoset(P,P), P means :Deffixfunc:
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[set,set] 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 st x in X ex y st y in Y & U[x,y]
proof
let x;
assume x in X;
then reconsider x as Element of ConPoset(P,P);
reconsider h = x as continuous Function of P, P by LemCastFunc01;
take y = least_fix_point h;
thus thesis;
end;
consider IT being Function of X,Y such that
A2: for x 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
A1: (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);
set Y = the carrier of P;
for x st x in X holds h1.x = h2.x
proof
let x;
assume x in X;
then reconsider g = x as Element of ConPoset(P,P);
reconsider h = g as continuous Function of P, P by LemCastFunc01;
h1.x = least_fix_point h by A1
.= h2.x by A1;
hence thesis;
end;
hence thesis by FUNCT_2:18;
end;
end;
LemFix01:
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 9;
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
B1: p1=g1 & p2=g2 & g1 <= g2 by A1,DefConRelat;
reconsider h1 = p1, h2 = p2 as continuous Function of P, P
by LemCastFunc01;
g1 = h1 by B1;
then reconsider g1 as continuous Function of P, P;
g2 = h2 by B1;
then reconsider g2 as continuous Function of P, P;
take g1,g2;
thus thesis by B1;
end;
hence thesis;
end;
LemFix0201:
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 B1:p1 <= p2;
let a, b be Element of P;
assume B2:a = IT.p1 & b = IT.p2;
consider g1,g2 being continuous Function of P,P such that
B3: p1=g1 & p2=g2 & g1 <= g2 by B1,LemFix01;
a = least_fix_point(g1) & b = least_fix_point(g2) by B2,Deffixfunc,B3;
hence thesis by B3,Thfixpoint02;
end;
hence thesis by ORDERS_3:def 5;
end;
LemFix02:
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;
LemFix0301:
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 A0: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
B1: 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 A0;
thus thesis by B1;
end;
hence thesis;
end;
LemFix03:
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 A0: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 set such that A1:g in G by XBOOLE_0:def 1;
reconsider g as Element of ConPoset(P,P) by A1;
reconsider gg = g as continuous Function of P,P by LemCastFunc01;
reconsider p = iter(gg,n).(Bottom P) as Element of P by Lemiter11;
A2:p in X by A0,A1;
x in X implies x in the carrier of P
proof
assume x in X;
then x is Element of the carrier of P by LemFix0301,A0;
hence thesis;
end;
hence thesis by TARSKI:def 3,A2;
end;
LemFix0401:
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 11;
per cases by A2,RELAT_2:def 7,A1;
suppose [f,g] in S;
then consider f1,g1 being Function of P,P such that
B1:f=f1 & g=g1 & f1 <= g1 by DefConRelat;
thus thesis by B1;
end;
suppose [g,f] in S;
then consider g1,f1 being Function of P,P such that
B2:g=g1 & f=f1 & g1 <= f1 by DefConRelat;
thus thesis by B2;
end;
end;
LemFix04:
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 A0: 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 A0,LemFix03;
x in X & y in X & x <>y implies [x,y] in R or [y,x] in R
proof
assume B1:x in X & y in X & x <>y;
consider p1 being Element of P,
g1 being continuous Function of P,P such that
B2: x=p1 & g1 in G & p1 = iter(g1,n).(Bottom P) by A0,B1,LemFix02;
consider p2 being Element of P,
g2 being continuous Function of P,P such that
B3: y=p2 & g2 in G & p2 = iter(g2,n).(Bottom P) by A0,B1,LemFix02;
per cases by B2,B3,LemFix0401;
suppose g1 <= g2;
then p1 <= p2 by Lemiter17,B2,B3;
hence thesis by B2,B3,ORDERS_2:def 9;
end;
suppose g2 <= g1;
then p2 <= p1 by Lemiter17,B2,B3;
hence thesis by B2,B3,ORDERS_2:def 9;
end;
end;
then A1:R is_connected_in X by RELAT_2:def 6;
x in X implies [x,x] in R
proof
assume x in X;
then reconsider x as Element of P;
x<=x;
hence thesis by ORDERS_2:def 9;
end;
then R is_reflexive_in X by RELAT_2:def 1;
then R is_strongly_connected_in X by A1,ORDERS_1:92;
hence thesis by ORDERS_2:def 11;
end;
LemFix0503:
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;
set y = h.x;
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 12;
end;
LemFix0504:
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 LemCastFunc02;
reconsider G1 = g1 as continuous Function of P,P;
p = least_fix_point(G1) by Deffixfunc,A1
.= sup iter_min(g) by Thfixpoint01;
hence thesis by Lem201,A2;
end;
LemFix0505:
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 st y in dom g1 & y in M & x = g1.y by FUNCT_1:def 12;
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;
LemFix05:
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 LemFix0201;
h.(sup G) <= sup (h.:G)
proof
reconsider L = h.:G as non empty Chain of P by ThChain1;
set g0 = sup G;
set p0 = h.g0;
reconsider G0 = g0 as continuous Function of P,P by LemCastFunc01;
B2:p0 = least_fix_point(G0) by Deffixfunc;
B3:sup G = sup_func(G) by ThConPoset01;
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 ThiterSet1;
B4: p0 = sup iter_min(g0) by Thfixpoint01,B2
.= sup I0;
B5:ex_sup_of I0,P by DefchainComplete;
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
C1: x=y & ex n being Nat st y = iter(g0,n).a;
consider n0 being Nat such that C2:x = iter(g0,n0).a by C1;
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 LemFix04;
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
D1: p=p0 & g in G & p0 = iter(g,n0).a by LemFix02;
set r = h.g;
r in L by D1,LemFix0503;
then reconsider r as Element of P;
D4:r <= sup L by Lem201,D1,LemFix0503;
p <= r by D1,LemFix0504;
hence thesis by D4,ORDERS_2:26;
end; then
C3: sup M0 <= sup L by Lem202;
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;
C4: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 Lemiter10;
hence thesis by YELLOW_0:44;
end;
C5: U[k] implies U[k+1]
proof
assume D1: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
E1: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 by Lemiter11;
E2:z1 = (g0*iter(g0,k)).a by E1,FUNCT_7:73
.= g0.z by Lemiter12;
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 LemFix04;
reconsider M0 = g0.:M as non empty Chain of P by ThChain1;
E3:g0.(sup M) = sup M0 by Thcontinuous01;
E401:ex_sup_of M0,P by DefchainComplete;
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
F1: g in G & q = g0.(iter(g,k).a) by LemFix0505;
reconsider a1 = iter(g,k).a as Element of P by Lemiter11;
reconsider W = G-image a1 as non empty Chain of P;
F2:q = sup W by F1,Defsupfunc,B3;
F3:ex_sup_of W,P by DefchainComplete;
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
F401: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 F402:g1 in G & q1=g1.a1 by F401;
per cases by F1,F402,LemFix0401;
suppose g1 <= g;
then F404:q1 <= g.a1 by YELLOW_2:10,F402;
set a2 = g.a1;
reconsider g2 = g as Element of ConPoset(P,P)
by LemCastFunc02;
reconsider gg = g2 as continuous Function of P,P;
a2 = (g*iter(g,k)).a by Lemiter12
.= iter(gg,k+1).a by FUNCT_7:73;
then a2 in M1 by E1,F1;
then a2 <= sup M1 by Lem201;
hence thesis by F404,ORDERS_2:26;
end;
suppose F405:g <= g1;
reconsider a2 = iter(g1,k).a as Element of P by Lemiter11;
a1 <= a2 by F405,Lemiter17;
then F406:q1 <= g1.a2 by ORDERS_3:def 5,F402;
set a3 = g1.a2;
reconsider g2 = g1 as Element of ConPoset(P,P)
by LemCastFunc02;
reconsider gg = g2 as continuous Function of P,P;
a3 = (g1*iter(g1,k)).a by Lemiter12
.= iter(gg,k+1).a by FUNCT_7:73;
then a3 in M1 by E1,F402;
then a3 <= sup M1 by Lem201;
hence thesis by F406,ORDERS_2:26;
end;
end;
then W is_<=_than sup M1 by LATTICE3:def 9;
hence thesis by F2,F3,YELLOW_0:def 9;
end;
then M0 is_<=_than sup M1 by LATTICE3:def 9;
then E4:sup M0 <= sup M1 by E401,YELLOW_0:def 9;
z <= sup M by D1;
then z1 <= sup M0 by E2,E3,ORDERS_3:def 5;
hence thesis by E4,ORDERS_2:26;
end;
hence thesis;
end;
U[k] from NAT_1:sch 2(C4,C5);
then x <= sup M0 by C2;
hence thesis by C3, ORDERS_2:26;
end;
then I0 is_<=_than sup L by LATTICE3:def 9;
hence thesis by B4,B5,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 LemFix0201;
for L be non empty Chain of ConPoset(P,P)
holds f.(sup L) <= sup (f.:L) by LemFix05;
hence thesis by Thcontinuous03;
end;
end;