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