:: Fix-point Theorem for Continuous Functions on Chain-complete Posets
:: by Kazuhisa Ishida and Yasunari Shidama
::
:: Received November 10, 2009
:: Copyright (c) 2009-2018 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;
begin
registration let P be non empty Poset; :: move to ORDERS_2
cluster non empty for Chain of P;
end;
definition let IT be RelStr;
attr IT is chain-complete means
:: POSET_1:def 1
IT is lower-bounded &
for L being Chain of IT st L is non empty holds ex_sup_of L,IT;
end;
theorem :: POSET_1:1
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;
registration
cluster strict chain-complete non empty for Poset;
end;
registration
cluster chain-complete -> lower-bounded for RelStr;
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 :: POSET_1:2
sup (f.:L) <= f.(sup L);
begin
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
:: POSET_1:def 2
{x where x is Element of P : ex n being Nat st x = iter(g,n).p};
end;
theorem :: POSET_1:3
iterSet(g,Bottom P) is non empty Chain of P;
definition let P; let g be monotone Function of P,P;
func iter_min(g) -> non empty Chain of P equals
:: POSET_1:def 3
iterSet(g,Bottom P);
end;
theorem :: POSET_1:4
sup iter_min(g) = sup (g.:iter_min(g));
theorem :: POSET_1:5
g1 <= g2 implies sup iter_min(g1) <= sup iter_min(g2);
:: 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
:: POSET_1:def 4
f is monotone & for L be non empty Chain of P holds f preserves_sup_of L;
end;
theorem :: POSET_1:6
for f being Function of P,Q holds f is continuous iff
(f is monotone & for L holds f.(sup L) = sup (f.:L));
theorem :: POSET_1:7
for z being Element of Q holds (P-->z) is continuous;
registration let P,Q;
cluster continuous for Function of P, Q;
end;
registration let P,Q;
cluster continuous -> monotone for Function of P, Q;
end;
theorem :: POSET_1:8
for f being monotone Function of P,Q holds
(for L holds f.(sup L) <= sup (f.:L)) implies f is continuous;
definition let P; let g be monotone Function of P,P;
assume g is continuous;
func least_fix_point(g) -> Element of P means
:: POSET_1:def 5
it is_a_fixpoint_of g & for p st p is_a_fixpoint_of g holds it <= p;
end;
theorem :: POSET_1:9
for g being continuous Function of P,P holds
least_fix_point(g) = sup iter_min(g);
theorem :: POSET_1:10
for g1,g2 being continuous Function of P,P st g1 <= g2 holds
least_fix_point(g1) <= least_fix_point(g2);
begin
:: 3. Function space of continuous functions on chain-complete Posets
definition let P,Q;
func ConFuncs (P,Q) -> non empty set equals
:: POSET_1:def 6
{x where x is Element of Funcs(the carrier of P,the carrier of Q)
:ex f be continuous Function of P,Q st f=x };
end;
definition let P,Q;
func ConRelat(P,Q) -> Relation of ConFuncs(P,Q) means
:: POSET_1:def 7
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);
end;
registration let P,Q;
cluster ConRelat(P,Q) -> reflexive;
cluster ConRelat(P,Q) -> transitive;
cluster ConRelat(P,Q) -> antisymmetric;
end;
definition let P,Q;
func ConPoset(P,Q) -> strict non empty Poset equals
:: POSET_1:def 8
RelStr(#ConFuncs(P,Q),ConRelat(P,Q)#);
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
:: POSET_1:def 9
{x where x is Element of Q
:ex f being continuous Function of P,Q st f in F & x=f.p};
end;
definition let P,Q,F;
func sup_func(F) -> Function of P,Q means
:: POSET_1:def 10
for p,M holds M=F-image p implies it.p=sup M;
end;
registration let P,Q,F;
cluster sup_func(F) -> continuous;
end;
theorem :: POSET_1:11
ex_sup_of F, ConPoset(P,Q) & sup_func(F) = "\/"(F,ConPoset(P,Q));
definition let P,Q;
func min_func(P,Q) -> Function of P,Q equals
:: POSET_1:def 11
P --> Bottom Q;
end;
registration let P,Q;
cluster min_func(P,Q) -> continuous;
end;
theorem :: POSET_1:12
for f being Element of ConPoset(P,Q) st f = min_func(P,Q)
holds f is_<=_than the carrier of ConPoset(P,Q);
registration let P,Q;
cluster ConPoset(P,Q) -> chain-complete;
end;
begin
definition let P;
func fix_func(P) -> Function of ConPoset(P,P), P means
:: POSET_1:def 12
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;
end;
registration let P;
cluster fix_func(P) -> continuous;
end;