:: Increasing and Continuous Ordinal Sequences :: by Grzegorz Bancerek :: :: Received May 31, 1990 :: Copyright (c) 1990-2021 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 ORDINAL2, ORDINAL1, FUNCT_1, XBOOLE_0, RELAT_1, TARSKI, ORDINAL3, SUBSET_1, CLASSES2, ZFMISC_1, CARD_1, ORDINAL4; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, ORDINAL2, ORDINAL3, CARD_1, CLASSES2; constructors WELLORD2, FUNCOP_1, ORDINAL3, CARD_1, CLASSES1, CLASSES2, RELSET_1; registrations XBOOLE_0, FUNCT_1, ORDINAL1, ORDINAL2, ORDINAL3, CARD_1, CLASSES2, RELSET_1; requirements SUBSET, BOOLE, NUMERALS; begin reserve phi,fi,psi for Ordinal-Sequence, A,A1,B,C,D for Ordinal, f,g for Function, X for set, x,y,z for object; registration let L be Ordinal-Sequence; cluster last L -> ordinal; end; theorem :: ORDINAL4:1 dom fi = succ A implies last fi is_limes_of fi & lim fi = last fi; definition let fi,psi be Sequence; func fi^psi -> Sequence means :: ORDINAL4:def 1 dom it = (dom fi)+^(dom psi) & (for A st A in dom fi holds it.A = fi.A) & for A st A in dom psi holds it.((dom fi) +^A) = psi.A; end; theorem :: ORDINAL4:2 for A, B being Sequence holds rng(A^B) = rng A \/ rng B; registration let fi,psi; cluster fi^psi -> Ordinal-yielding; end; theorem :: ORDINAL4:3 A is_limes_of psi implies A is_limes_of fi^psi; theorem :: ORDINAL4:4 A is_limes_of fi implies B+^A is_limes_of B+^fi; theorem :: ORDINAL4:5 A is_limes_of fi implies A*^B is_limes_of fi*^B; theorem :: ORDINAL4:6 dom fi = dom psi & B is_limes_of fi & C is_limes_of psi & ((for A st A in dom fi holds fi.A c= psi.A) or for A st A in dom fi holds fi.A in psi.A ) implies B c= C; reserve f1,f2 for Ordinal-Sequence; theorem :: ORDINAL4:7 dom f1 = dom fi & dom fi = dom f2 & A is_limes_of f1 & A is_limes_of f2 & (for A st A in dom fi holds f1.A c= fi.A & fi.A c= f2.A) implies A is_limes_of fi; theorem :: ORDINAL4:8 dom fi <> {} & dom fi is limit_ordinal & fi is increasing implies sup fi is_limes_of fi & lim fi = sup fi; theorem :: ORDINAL4:9 fi is increasing & A c= B & B in dom fi implies fi.A c= fi.B; theorem :: ORDINAL4:10 fi is increasing & A in dom fi implies A c= fi.A; theorem :: ORDINAL4:11 phi is increasing implies phi"A is epsilon-transitive epsilon-connected set; theorem :: ORDINAL4:12 f1 is increasing implies f2*f1 is Ordinal-Sequence; theorem :: ORDINAL4:13 f1 is increasing & f2 is increasing implies ex phi st phi = f1* f2 & phi is increasing; theorem :: ORDINAL4:14 f1 is increasing & A is_limes_of f2 & sup rng f1 = dom f2 & fi = f2*f1 implies A is_limes_of fi; theorem :: ORDINAL4:15 phi is increasing implies phi|A is increasing; theorem :: ORDINAL4:16 phi is increasing & dom phi is limit_ordinal implies sup phi is limit_ordinal ; theorem :: ORDINAL4:17 fi is increasing & fi is continuous & psi is continuous & phi = psi*fi implies phi is continuous; theorem :: ORDINAL4:18 (for A st A in dom fi holds fi.A = C+^A) implies fi is increasing; theorem :: ORDINAL4:19 C <> {} & (for A st A in dom fi holds fi.A = A*^C) implies fi is increasing; theorem :: ORDINAL4:20 A <> {} implies exp({},A) = {}; theorem :: ORDINAL4:21 A <> {} & A is limit_ordinal implies for fi st dom fi = A & for B st B in A holds fi.B = exp(C,B) holds exp(C,A) is_limes_of fi; theorem :: ORDINAL4:22 C <> {} implies exp(C,A) <> {}; theorem :: ORDINAL4:23 1 in C implies exp(C,A) in exp(C,succ A); theorem :: ORDINAL4:24 1 in C & A in B implies exp(C,A) in exp(C,B); theorem :: ORDINAL4:25 1 in C & (for A st A in dom fi holds fi.A = exp(C,A)) implies fi is increasing; theorem :: ORDINAL4:26 1 in C & A <> {} & A is limit_ordinal implies for fi st dom fi = A & for B st B in A holds fi.B = exp(C,B) holds exp(C,A) = sup fi; theorem :: ORDINAL4:27 C <> {} & A c= B implies exp(C,A) c= exp(C,B); theorem :: ORDINAL4:28 A c= B implies exp(A,C) c= exp(B,C); theorem :: ORDINAL4:29 1 in C & A <> {} implies 1 in exp(C,A); theorem :: ORDINAL4:30 exp(C,A+^B) = exp(C,B)*^exp(C,A); theorem :: ORDINAL4:31 exp(exp(C,A),B) = exp(C,B*^A); theorem :: ORDINAL4:32 1 in C implies A c= exp(C,A); ::$N Fixed-point lemma for normal functions scheme :: ORDINAL4:sch 1 CriticalNumber { phi(Ordinal) -> Ordinal } : ex A st phi(A) = A provided for A,B st A in B holds phi(A) in phi(B) and for A st A <> {} & A is limit_ordinal for phi st dom phi = A & for B st B in A holds phi.B = phi(B) holds phi(A) is_limes_of phi; reserve W for Universe; registration let W; cluster ordinal for Element of W; end; definition let W; mode Ordinal of W is ordinal Element of W; mode Ordinal-Sequence of W is Function of On W, On W; end; registration let W; cluster non empty for Ordinal of W; end; registration let W; cluster On W -> non empty; end; registration let W; cluster -> Sequence-like Ordinal-yielding for Ordinal-Sequence of W; end; reserve A1,B1 for Ordinal of W, phi for Ordinal-Sequence of W; scheme :: ORDINAL4:sch 2 UOSLambda { W() -> Universe, F(set) -> Ordinal of W() } : ex phi being Ordinal-Sequence of W() st for a being Ordinal of W() holds phi.a = F(a); definition let W; func 0-element_of W -> Ordinal of W equals :: ORDINAL4:def 2 {}; func 1-element_of W -> non empty Ordinal of W equals :: ORDINAL4:def 3 1; let phi,A1; redefine func phi.A1 -> Ordinal of W; end; definition let W; let p2,p1 be Ordinal-Sequence of W; redefine func p1*p2 -> Ordinal-Sequence of W; end; theorem :: ORDINAL4:33 0-element_of W = {} & 1-element_of W = 1; definition let W,A1; redefine func succ A1 -> non empty Ordinal of W; let B1; redefine func A1 +^ B1 -> Ordinal of W; end; definition let W,A1,B1; redefine func A1 *^ B1 -> Ordinal of W; end; theorem :: ORDINAL4:34 A1 in dom phi; theorem :: ORDINAL4:35 dom fi in W & rng fi c= W implies sup fi in W; reserve L for Sequence; theorem :: ORDINAL4:36 phi is increasing & phi is continuous & omega in W implies ex A st A in dom phi & phi.A = A; begin :: Addenda :: from ZFREFLE1, 2007.03.14, A.T. reserve e,u for set; theorem :: ORDINAL4:37 A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C; theorem :: ORDINAL4:38 A is_cofinal_with B implies (A is limit_ordinal iff B is limit_ordinal ); :: from 2009.09.28, A.T. registration let D; let f,g be Sequence of D; cluster f^g -> D-valued; end; theorem :: ORDINAL4:39 for A, B being Sequence holds rng A c= rng(A^B); theorem :: ORDINAL4:40 for A, B being Sequence holds rng B c= rng(A^B);