|
Hello there dear MIZAR enthusiasts!
My name is Sebastian Koch, I started learning MIZAR around spring 2016 and by now, after submitting my first article and drafting a second, I think I can write one thing or two in this mailing list :-) The mail got longer than I anticipated, so if you are short on time, just skip to the bold parts.
I strongly believe in MIZAR as humanity's best attempt at the QED manifesto and I would like to spread the ideology ;) i.e. make more people believe that it is a good thing to formalize mathematics in MIZAR. However, there is a simple yet powerful reason for people not to do it:
MIZAR is extremly difficult.
To be more precise, it isn't the language itself that proves to be difficult but the elements around it, all foremost the large size of the MML. (Other reasons are e.g. outdated documentation and broken links.) There are several (outdated but still mostly valid) documentations about how an article is written, but I failed to find one about where in the MML I can find what. At first glance a beginner would tend to think that the article names would be givaways of their content, but then he hasn't recognized the WAYBEL and YELLOW series yet. And how in all likability would one (read: undergraduate) come to think of searching for binomial coefficients in an article named NEWTON?
There are about two ways to get to know the MML in (somewhat) order: Starting with reading the old "Formalized Mathematics" journals (as I did at the beginning), where the fundamental understanding of mathematics and analysis is soon obscured by the theory of lattices and other articles that are not part of de facto standard courses to learn mathematics. Adding to that, the articles in the MML are constantly changed by the library committee, so one cannot completely trust the old articles from the 90's. The other way is looking at mml.lar to see the order of how MML articles are included to get a reading order and skipping those which turn out to be (momentarily) uninteresting, when browsing through the HTML articles.
(By the way, if you know other ways introductions to the MML, let me know.)
Of course there are the simple tools like findvoc or grep which are de facto the only tools beside the sophisticated MML Query page (which has it own flaws) and it was what I used then, only to be always surprised again what existing constructs I missed
by change. And when that happens, one can either ignore existing structures creating redundancies in the MML or overwork the whole article (I did the latter). This can easily make less devoted ethusiasts look for other projects which are easier to get into.
I want to create an approach to the MML for newcomers and I'm looking for help.
The basic idea is to take a classical book for an undergraduate course in mathematics and create a "mapping" between the content of the book (definitions, theorems, also site notes) and the content of the MML.
I created a mapping for testing purposes for the first two chapters of [1] (attached). I chose [1] simply because it is my standard/favourite Analysis book and I'm used to it. Since the first undergraduate courses in Germany are usually given in German,
[1] is also in the German language and so is my first mapping, but since it implies the user has the book and the MML available, it is short, so I have no doubt you get the basic idea when you have a look inside it even if you don't understand German. Btw
I used an artifical mark-up (§§ for hyperlinks, €€ for inline-MIZAR, #[] for MIZAR paragraphs and $$ for usual LaTeX math) to have it preparsed to LaTeX later on.
Given a (standard?) undergraduate book in the English language for Analysis or Linear Algebra, I would like to create such a mapping to the MML to provide MIZAR beginners with some orientation where to start.
Hardly seen in my attached example (for example in line 280) is that constructions/mechanisms in the MML should be explained where appropiate as well (for example that in MIZAR addition etc. over reals is introduced by addition over complex numbers, in opposite to [1]). This would happen to a greater extend when chapter 4 of [1] would be mapped: Functions are introduced in the sense of €Function of X, COMPLEX€ where €X€ is a set; there I would first explain the "hierarcy" of relations, partial functions and then functions in MIZAR.
Creating a mapping consists roughly of 3 parts: 1. Find the appropiate definitions/theorems/clusters in the MML 2. Explain differences to the book or construction mechanisms of MIZAR where appropiate. For example I cite right at the beginning €ORDINAL1:def 12€ to show what a natural number in MIZAR is without ever going to explain ordinal numbers at all, since this is not part of the book. 3. Nicely format the mapping and explanations into a PDF via LaTeX.
I could need help with the following: A) Recommendation of books to map. Something of international standard if there is anything like that. B) Help with the mapping itself. Simply because it is some work and needs time to be done. I can do that all alone, too, although I might miss some theorem in the MML and mark it as {no equivalent} in the mapping, compare line 260 in the attachment. Exercise 2 on p. 6 from [1] is the recursion formula of the power sums found by Pascal, which I couldn't find in the MML. C) Someone to look over the explanations regarding the differences between the book and MIZAR.
For example, I might explain that €COMPLEX€ is defined the way it is defined so that €REAL c= COMPLEX€ is simply true. If my reasoning is wrong (although reasonable (or not reasonable at all)), I would like someone to point it out.
D) Someone to bring the mapping into LaTeX. I think formatted output would be nice, but I also think that a mark-up version would fulfill the purpose of an approach to the MML, so I won't bother doing that except for preparsing.
Best regards Sebastian Koch
[1] Analysis 1, Konrad Königsberger, 6th edition,
http://www.springer.com/us/book/9783540403715 |
Mapping Königsberger -> MIZAR
# Natürliche Zahlen und vollständige Induktion
#~ Natürliche Zahlen, die im Gegensatz zu KNG mit Null statt mit 1 beginnen:
#[NUMBERS]
notation
synonym NAT for omega;
end;
#[ORDINAL1]
definition
let A be object;
attr A is natural means
:: ORDINAL1:def 12
A in omega;
end;
#[NAT_1]
definition
mode Nat is natural number;
end;
#[ORDINAL1]
definition
let x be Number;
attr x is zero means
:: ORDINAL1:def 14
x = 0;
end;
auÃ?erdem
#[]
requirements NUMERALS, ARITHM;
und zum �environment� �NUMBERS�, �ORDINAL1�, �CARD_1� und �NAT_1� hinzufügen
Für eine natürliche Zahl im Sinne von KNG würde man dann �non zero Nat� schreiben, z.B.
#[]
for n being non zero Nat holds 0 < n;
Im Ã?brigen sind folgende Schreibweisen aufgrund des Clusterings identisch:
#[]
for n being Nat {...}
for n being natural number {...}
for n being Element of NAT {...}
#~ Vollständige Induktion:
#[NAT_1]
scheme :: NAT_1:sch 2
NatInd { P[Nat] } : for k being Nat holds P[k]
provided
P[0] and
for k be Nat st P[k] holds P[k + 1];
Wenn man vollständige Induktion mit diesem Scheme bei 1 beginnen lassen möchte für eine Eigenschaft �Q[Nat]�, würde man etwas schreiben wie
#[]
defpred P[Nat] means 1 <= $1 & P[$1]
Eine elegantere Alternative hierfür wäre
#[NAT_1]
scheme :: NAT_1:sch 10
Indfrom1 { P[Nat] } : for k being non zero Nat holds P[k]
provided
( P[1]) and
for k being non zero Nat st P[k] holds P[k + 1];
oder
#[NAT_1]
scheme :: NAT_1:sch 8
Ind1{M() -> Nat, P[Nat]} : for i being Nat st M() <= i holds P[i]
provided
P[M()] and
for j being Nat st M() <= j holds P[j] implies P[j+1];
Zwei weitere wichtige Induktionsvarianten, die in Abschnitt 1.1 von KNG nicht erwähnt werden, sind
#[NAT_1]
scheme :: NAT_1:sch 4
CompInd { P[Nat] } : for k being Nat holds P[k]
provided
for k being Nat st for n being Nat st n < k holds P[n] holds P[k];
#[NAT_1]
scheme :: NAT_1:sch 7
Regr { P[Nat] } : P[0]
provided
ex k being Nat st P[k] and
for k being Nat st k <> 0 & P[k] ex n being Nat st n < k & P[n];
Die Gauss-Summe findet sich in
#[NUMPOLY1]
definition let n be Nat;
func Triangle n -> Real equals
:: NUMPOLY1:def 1
Sum idseq n;
end;
#[NUMPOLY1]
theorem :: NUMPOLY1:19
Triangle n = n * (n + 1) / 2;
und wird tatsächlich mit �NAT_1:sch 2� bewiesen, siehe §http://mizar.org/version/current/html/numpoly1.html#T19§;.
Die geometrische Summenformel findet sich in
#[COMSEQ_3]
definition
let z be Complex;
func z GeoSeq -> Complex_Sequence means
:: COMSEQ_3:def 1
it.0 = 1r & for n holds it.(n+1) = it.n * z;
end;
#[COMSEQ_3]
theorem :: COMSEQ_3:36
1r <> z implies for n holds Partial_Sums(z GeoSeq).n = (1r - z
|^ (n+1))/(1r-z);
und der Beweis benutzt ebenfalls �NAT_1:sch 2�, siehe §http://mizar.org/version/current/html/comseq_3.html#T36§;.
#~ Das Prinzip der rekursiven Definition
Die rekursive Definition im Sinne von KNG findet sich in
#[NAT_1]
scheme :: NAT_1:sch 11
LambdaRecEx{A() -> object,G(object,object) -> object}:
ex f being Function st dom f = NAT & f.0 = A() &
for n being Nat holds f.(n+1) = G(n,f.n);
#[NAT_1]
scheme :: NAT_1:sch 12
LambdaRecExD{D() -> non empty set, A() -> Element of D(),
G(object,object) -> Element of D()}:
ex f being sequence of D() st f.0 = A() & for n being Nat
holds f.(n+1) = G(n,f.n);
Es wirkt so, als ob dies nur Zugriff auf den vorherigen Wert bietet, aber der Schein trügt (siehe etwa Definition der Fibonacci-Zahlen in §http://mizar.org/version/current/html/pre_ff.html#K1§;). In der Praxis wird meist eine Folge definiert, die die gewünschten Eigenschaften hat (d.h. die Folge stellt die rekursive Definition dar), und dann wird lediglich die Existenz der Folge bewiesen. Ein Beispiel sahen wir bereits oben bei der Definition von �GeoSeq�, der Existenzbeweis nutzt tatsächlich �NAT_1:sch 12� (siehe §http://mizar.org/version/current/html/comseq_3.html#K1§;), ein anderes ist durch die Finbonacci-Zahlen gegeben.
Potenzen (mit natürlichem Exponenten) siehe übrigens:
[#NEWTON]
definition
let x be Complex, n be natural Number;
func x |^ n -> set equals
:: NEWTON:def 1
Product (n |-> x);
end;
[#NEWTON]
registration
let x be Real, n be natural Number;
cluster x |^ n -> real;
end;
[#NEWTON]
registration
let z be Complex, n be natural Number;
cluster z|^n -> complex;
end;
#~ Fakultät und Binomialkoeffizient
Definition Fakultät:
[#NEWTON]
definition
let n be natural Number;
func n! -> set equals
:: NEWTON:def 2
Product idseq n;
end;
[#NEWTON]
registration
let n be natural Number;
cluster n! -> real;
end;
Definition Permutation einer Menge:
#[FUNCT_2]
definition
let X;
mode Permutation of X is bijective Function of X,X;
end;
Satz 1': Die Anzahl der Permutationen von n verschiedenen Elementen ist $n!$
#[CARD_FIN]
theorem :: CARD_FIN:8
card{F where F is Function of X,X : F is Permutation of X} = (card X)!;
Definition Binomialkoeffizient:
#[NEWTON]
definition
let k,n be natural Number;
func n choose k -> set means
:: NEWTON:def 3
for l be Nat st l = n-k holds it = (n!)/((k!) * (l!)) if n >= k
otherwise it = 0;
end;
#[NEWTON]
registration
let k,n be natural Number;
cluster n choose k -> real;
end;
Randwerte stehen in â?¬NEWTON:19â?¬ und â?¬NEWTON:21â?¬, Rekursionsformel ist â?¬NEWTON:22â?¬ und dann ist da noch
#[NEWTON]
theorem :: NEWTON:20
s >= t & r = s-t implies s choose t = s choose r;
Satz 2: Die Anzahl von $k$-elementigen Teilmengen einer $n$-elementingen Menge ist $n$ über $k$:
#[CARD_FIN]
definition
let X,k; let x1,x2 be object;
func Choose(X,k,x1,x2) -> Subset of Funcs(X,{x1,x2}) means
:: CARD_FIN:def 1
x in it iff ex f be Function of X,{x1,x2} st f = x & card (f"{x1})=k;
end;
#[CARD_FIN]
theorem :: CARD_FIN:16
for x,y being object holds
x <> y implies card Choose(X,k,x,y) = (card X) choose k;
Satz 3: Binomischer Lehrsatz (in $\mathbb{R})
#[NEWTON]
definition
let a,b be Real;
let n be natural Number;
func (a,b) In_Power n -> FinSequence of REAL means
:: NEWTON:def 4
len it = n+1 & for i,l,m being Nat st i in dom it & m = i - 1 & l = n-m holds
it.i = (n choose m) * a|^l * b|^m;
end;
#[NEWTON]
theorem :: NEWTON:30
(a+b) |^ s = Sum((a,b) In_Power s);
#~ Aufgaben:
#~~ 1. a) & b) und 2.
Allgemein werden in �NUMPOLY1� die Polygon-Zahlen eingeführt. b) ist �NUMPOLY1:59�, a) und 2. scheinen nicht in der MML zu sein. �bung!
#~~ 3.
Ist â?¬NEWTON:32â?¬.
#~~ 4.
Allgemeiner auch für unendliche Mengen in �CARD_2:31�
#~~ 8.
Allgemeiner auch für unendliche Mengen in �FINSEQ_4:65�.
#~~ 1. c), 5. bis 7., 9.
{nicht in der MML gesucht}
# Reelle Zahlen
In KNG werden die Grundbegriffe der Zahlenbereiche vorausgesetzt. Die Zahlenbereichs-Hierarchie kann man
�NUMBERS� entnehmen. Die Abgeschlossenheit der Grundrechenoperationen im jeweiligen Zahlenbereich finden sich in �NAT_1� (für $\mathbb{N}$), �INT_1� (für $\mathbb{Z}$), �RAT_1� (für $\mathbb{Q}$) und �REAL_1� bzw. �XREAL_0� (für $\mathbb{R}$). Konstruktion von $\mathbb{N}$ ist �ORDINAL1:def 11�, $\mathbb{Z}$ ist �NUMBERS:def 4�, $\mathbb{Q}_+$ ist �ARYTM_3:def 7�, $\mathbb{Q}$ ist �NUMBERS:def 3�, $\mathbb{R}_+$ ist �ARYTM_2:def 2� (über Dedekindsche Schnitte, Def. �ARYTM_2:def 1�) und $\mathbb{R}$ ist �NUMBERS:def 1�.
Es ist anzumerken, dass über ein Jahrzehnt gedauert hat, bis die reellen Zahlen klar definiert in der MML waren. Vorher wurden ihre Eigenschaften über Axiome (�AXIOMS�) vorgegeben, damit in dieser Zeit andere Artikel mit reellen Zahlen einfach schon geschrieben werden konnten. Dies erklärt auch, warum die Jahreszahlen der Artikel und ihr inhaltlicher Aufbau auf anderen Artikeln so wirr wirken können.
Wer mit reellen Zahlen arbeiten will, sollte â?¬REALâ?¬ in seinen â?¬requirementsâ?¬ haben.
#~ Die Körperstruktur von \mathbb{R}
Die Grundrechenoperationen werden über komplexe Zahlen (Def. �NUMBERS:def 2�) in �XCMPLX_0� eingeführt, da sich die Eigenschaften von $\mathbb{C}$ auf $\mathbb{R}$ vererben, sind die Körperaxiome von $\mathbb{R}$ in folgender Weise abgedeckt:
* Kommutativität von Addition und Multiplikation: Durch das Schlüsselwort �commutativity� in �XCMPLX_0:def 4� und �XCMPLX_0:def 5� gedeckt.
* Assoziativität von Addition und Multiplikation: �XCMPLX_1:1� und �XCMPLX_1:4�
* Lösbarkeit der Gleichungen $a+x=b$ bzw. $ax=b$ (falls $a\neq 0$): setze $x=b-a$ und dann �XCMPLX_1:29�, �XCMPLX_1:14�, �ARITHM:1� bzw. setze $x=b/a$ und dann 2x �XCMPLX_1:74� (Kommutativität automatisch), �XCMPLX_1:60�, �ARITHM:3�.
* Distributivgesetz: â?¬XCMPLX_1:8â?¬
Es sei noch einmal angemerkt, dass MIZAR diese Schritte im Wesentlichen autonom durchführen kann. Die grundlegenden Rechengesetze finden sich in �XCMPLX_1�.
#~ Die Anordnung von $\mathbb{R}$
Die Anordnung auf $\mathbb{R}$ wird von der Anordnung auf $\mathbb{R}\cup{-\infty,+\infty}$ geerbt.
#[XXREAL_0]
definition
redefine func ExtREAL equals
:: XXREAL_0:def 4
REAL \/ {+infty,-infty};
end;
â?¬XXREAL_0:def 5â?¬ definiert $\leq$ auf â?¬ExtRealâ?¬ und sagt
\[x \leq y :\Longleftrightarrow \left\{ \begin{array}{rl}
x \leq y & \mbox{falls } x,y\in\mathbb{R}_+ \\
-y \leq -x & \mbox{falls } -x,-y\in\mathbb{R}_+ \\
(x\in\mathbb{R}_- & y\in\mathbb{R}_+) \vee x = -\infty \vee y = +\infty & \mbox{sonst}
\end{array}\right.\]
wobei $\leq$ auf der rechten Seite schon zuvor für $\mathbb{R}_+$ definiert wurde in $ARYTM_2:def 5$, welches wiederum auf die Vergleichbarkeit positiver rationaler Zahlen zurückgeht:
[#ARYTM_3]
definition
let x,y be Element of RAT+;
pred x <=' y means
:: ARYTM_3:def 13
ex z being Element of RAT+ st y = x+z;
connectedness;
end;
Die anderen Vergleichsoperatoren werden dann über Notation eingeführt:
#[XXREAL_0]
notation
let a,b be ExtReal;
synonym b >= a for a <= b;
antonym b < a for a <= b;
antonym a > b for a <= b;
end;
Positivität/Negativität ist weiter definiert als
#[XXREAL_0]
definition
let a be ExtReal;
attr a is positive means
:: XXREAL_0:def 6
a > 0;
attr a is negative means
:: XXREAL_0:def 7
a < 0;
end;
Anordnungsaxiom A1 folgt dann aus
#[XXREAL_0]
registration
cluster positive -> non negative non zero for ExtReal;
cluster non negative non zero -> positive for ExtReal;
cluster negative -> non positive non zero for ExtReal;
cluster non positive non zero -> negative for ExtReal;
cluster zero -> non negative non positive for ExtReal;
cluster non negative non positive -> zero for ExtReal;
end;
Anordnungsaxiom A2 folgt aus
#[XXREAL_3]
registration
let x be positive ExtReal;
let y be non negative ExtReal;
cluster x + y -> positive;
cluster y + x -> positive;
end;
#[XXREAL_3]
registration
let x,y be positive ExtReal;
cluster x*y -> positive;
end;
Anordnungsaxiom A3 kann gefolgert werden aus
[#GAUSSINT]
theorem :: GAUSSINT:48
for q be Element of REAL ex m be Element of INT st |.q - m .| <= 1/2;
Denn falls $m < 1$ wähle $n = 1$, sonst $n = m + 1$. Ferner ist $a > b \Longrightarrow a-b > 0$ durch �XREAL_1:50�, Rückrichtung kommt z.B. durch �XREAL_1:44�.
Zu den Rechenregeln:
1. steckt in â?¬XXREAL_0:1â?¬, denn $A\rightarrow B \Leftrightarrow \neg A \vee B$.
2. â?¬XXREAL_0:2â?¬
3. (â?¬XREAL_1:87â?¬ und â?¬XREAL_1:88â?¬), â?¬XREAL_1:6â?¬, (â?¬XREAL_1:68â?¬ und â?¬XREAL_1:69â?¬)
4. â?¬XREAL_1:8â?¬ und â?¬XREAL_1:66â?¬
5. (�XREAL_1:129� und �XREAL_1:130�) oder für $\leq$ gleich �XREAL_1:63�
6. �cluster -> non negative� in �NAT_1�, mit den Clustern oben aus �XXREAL_0� ergänzt sich das zum Gewünschten für natürliche Zahlen grö�er Null.
Bernoulli'sche Ungleichung: In der Form mit $\leq$ in â?¬PREPOWER:16â?¬ oder â?¬POWER:49â?¬
Satz 1: {nicht in MML gesucht}
Definition Absolutbetrag
#[ABSVALUE]
definition
let x be Real;
redefine func |.x.| equals
:: ABSVALUE:def 1
x if 0 <= x otherwise -x;
end;
Die eigentliche Definition ist aus â?¬COMPLEX1:def 12â?¬ Die vier Rechenregeln sind daher zu finden unter â?¬ABSVALUE:4â?¬, â?¬COMPLEX1:65â?¬, â?¬COMPLEX1:56â?¬, â?¬COMPLEX1:64â?¬.
#~ Vollständigkeit von $\mathbb{R}$
Intervalldefinitionen:
#[XXREAL_1]
definition
let r,s be ExtReal;
func [.r,s.] -> set equals
:: XXREAL_1:def 1
{ a : r <= a & a <= s };
func [.r,s.[ -> set equals
:: XXREAL_1:def 2
{ a : r <= a & a < s };
func ].r,s.] -> set equals
:: XXREAL_1:def 3
{ a : r < a & a <= s };
func ].r,s.[ -> set equals
:: XXREAL_1:def 4
{ a : r < a & a < s };
end;
Intervallverschachtelungen: {nicht in MML gesucht}
Satz 2 (Existenz von positiven Wurzeln): steckt in Existenzbeweis von â?¬PREPOWER:def 2â?¬.
Obere / untere Schranken:
#[XXREAL_2]
definition
let X be ext-real-membered set;
mode UpperBound of X -> ExtReal means
:: XXREAL_2:def 1
x in X implies x <= it;
mode LowerBound of X -> ExtReal means
:: XXREAL_2:def 2
x in X implies it <= x;
end;
Nach oben/unten beschränkt:
#[XXREAL_2]
definition
let X be ext-real-membered set;
attr X is bounded_below means
:: XXREAL_2:def 9
ex r being Real st r is LowerBound of X;
attr X is bounded_above means
:: XXREAL_2:def 10
ex r being Real st r is UpperBound of X;
end;
#[XXREAL_2]
definition
let X be ext-real-membered set;
attr X is real-bounded means
:: XXREAL_2:def 11
X is bounded_below bounded_above;
end;
Supremum/Infinum:
#[XXREAL_2]
definition
let X be ext-real-membered set;
func sup X -> ExtReal means
:: XXREAL_2:def 3
it is UpperBound of X & for x being UpperBound of X holds it <= x;
func inf X -> ExtReal means
:: XXREAL_2:def 4
it is LowerBound of X & for x being LowerBound of X holds x <= it;
end;
Beispiele:
1. â?¬XXREAL_2:25â?¬ bis â?¬XXREAL_2:32â?¬
2. Minimum und Maximum sind über Supremum und Infinum in �XXREAL_2:def 7� und �XXREAL_2:def 8� definiert.
3. Aus dem nachfolgenden Cluster folgt, dass unendliche Teilmengen von $\mathbb{N}$ nicht nach oben beschränkt sind, insbesondere also nicht $\mathbb{N}$ selbst. Die Unendlichkeit von $\mathbb{N}$ ist dabei in �CARD_1� geclustert.
#[XXREAL_2]
registration
cluster -> finite for bounded_above natural-membered set;
end;
#[CARD_1]
registration
cluster omega -> infinite;
end;
Satz 3: Die Definition von $\sup$ und $\inf$ in MIZAR sehen $+\infty$ und $-\infty$ als gültige Werte an, der Satz bedeutet in MIZAR also, dass $\sup$ und $\inf$ reell sind. Dies ist gegeben durch
#[XXREAL_2]
registration
let X be bounded_above non empty real-membered set;
cluster sup X -> real;
end;
#[XXREAL_2]
registration
let X be bounded_below non empty real-membered set;
cluster inf X -> real;
end;
Satz 4: Entsprechend zum vorherigen Satz wollen wir nun, dass $\max$ und $\min$ ganze Zahlen sind. Dabei bezeichnet â?¬left_endâ?¬ bzw. â?¬right_endâ?¬, dass das Infinum bzw. Supremum in der Menge enthalten ist.
#[XXREAL_2]
registration
cluster bounded_above -> right_end for non empty integer-membered set;
end;
#[XXREAL_2]
registration
cluster bounded_below -> left_end for non empty integer-membered set;
end;
#[XXREAL_2]
registration
let X be left_end integer-membered set;
cluster min X -> integer;
end;
#[XXREAL_2]
registration
let X be right_end integer-membered set;
cluster max X -> integer;
end;
Satz 5 ist â?¬RAT_1:7â?¬.
#~ $\mathbb{R}$ ist nicht abzählbar
Definition höchstens abzählbar und abzählbar unendlich:
#[CARD_3]
definition
let X;
attr X is countable means
:: CARD_3:def 14
card X c= omega;
attr X is denumerable means
:: CARD_3:def 15
card X = omega;
end;
#[CARD_3]
registration
cluster denumerable -> countable infinite for set;
cluster countable infinite -> denumerable for set;
end;
In der Praxis wird oftmals einfach â?¬card X = omegaâ?¬ anstatt der Attributdefinition verwendet.
$\mathbb{Z}$ ist abzählbar: �TOPGEN_3:16�
Satz 6: $\mathbb{Q}$ ist abzählbar: �TOPGEN_3:17�
Die Vereinigung abzählbarer Mengen ist abzählbar: �CARD_4:12�
Satz 7: $\mathbb{R}$ ist nicht abzählbar: �TOPGEN_3:def 4� und �TOPGEN_3:30� in Verbindung mit �CARD_1:3�
Folgerung: $\mathbb{R}\setminus\mathbb{Q}$ ist nicht abzählbar: nicht in MML, folgt aus den vorherigen Ergebnissen in Verbindung mit �CARD_2:98�, �CARD_2:76� und �NUMBERS:12�.
#~ Aufgaben:
1. Scheinbar nicht in MML, Ã?bung!
2. (â?¬PREPOWER:28â?¬ oder â?¬POWER:17â?¬) und {nicht in MML gesucht}
3. bis 15. {nicht in MML gesucht}
# Komplexe Zahlen