Mizarkommentare zu Gerd Fischers Lineare Algebra/ Grundbegriffe

1.1 Mengen und AbbildungenBearbeiten

1.1.1.Bearbeiten

Mizar verfügt über keine  -Notation für Mengen.   ist {x} (TARSKI:def 1),   ist {x,y} (TARSKI:def 3) und für explizit angegebene Mengen mit 3 bis 10 Elementen siehe ENUMSET1:def 1-8.   ist x in X aus HIDDEN (und damit immer ohne Referenz verfügbar). paarweise verschieden ist are_mutually_distinct und nur für 3 bis 7 Elemente in ZFMISC:def 5-9 definiert. Die (möglicherweise unendliche) Anzahl der Elemente einer Menge   ist card X (CARD_1:def 2), die Anzahl der Elemente der explizit angegebenen Mengen (mit 0 bis 7 paarweise verschieden Elementen) ist CARD_1:27 ( ), CARD_1:30 ( ), CARD_2:57,58,59 ( ), CARD_2:63 ( ) und BORSUK_5:3,4 ( ). Die Eigenschaft einer Menge, endlich zu sein, ist finite (FINSET_1:def 1).

Die leere Menge ist {} (XBOOLE_0:def 2) und die Eigenschaft einer Menge, leer zu sein, ist empty. Mit den üblichen requirements wird der Term X = {} genau so behandelt wie X is empty.

  ist X c= Y (TARSKI:def 3) und   ist in XBOOLE_0:def 10 definiert.

  wird in ORDINAL1:def 11 als omega eingeführt, das Synonym NAT wird in NUMBERS vergeben. Prinzip der vollständigen Induktion für Aussagen allgemein ist NAT_1:sch 2, aber keine Referenz für die nachfolgende, konkrete Aussage mit  . Die Null, die in Mizar mit der leeren Menge identifiziert wird (ORDINAL1:def 13), ist nach Definition in NAT enthalten;   ist NATPLUS (NAT_LAT:def 6).

  ist INT (INT_1:def 1 oder NUMBERS:def 4) und   ist RAT (RAT_1:def 1 oder NUMBERS:def 3).   ist REAL (NUMBERS:def 1): In Mizar werden die nichtnegativen reellen Zahlen über Dedekind-Schnitte eingeführt, siehe dafür ARYTM_2.   ist COMPLEX (NUMBERS:def 2), die Inklusionskette ist durch NUMBERS:17,14,12,11 gegeben.

1.1.2.Bearbeiten

Für eine Eigenschaft  , die in Mizar zuvor mit defpred festgelegt wurde, entspricht   dem Ausdruck { x where x is Element of X : P[x] }, welcher fest ins System eingebaut ist. Eine Variante hiervon ist die Notation the set of all x where x is special Element of X, wobei special stellvertretend für ein oder mehrere Attribute steht. Dies wird beispielsweise verwendet bei der Definition der Menge aller geraden Zahlen EvenNAT (FIB_NUM2:def 3).

Ähnlich zu 1.1.1. besitzt Mizar keine  -Notation für Vereingung bzw. Schnitt einer endlichen Anzahl von Mengen. Aber   ist X \/ Y (XBOOLE_0:def 3) und   ist X /\ Y (XBOOLE_0:def 4).

Das Konzept einer durch eine Indexmenge   induzierten Mengenfamilie   wird durch ManySortedSet beschrieben, welches einfach eine total I-defined Function (PBOOLE) ist (d.h. der Definitionsbereich der Abbildung ist ganz  ). Dieses Konzept wird aber gar nicht benötigt, da allgemeine Vereingung bzw. Schnitt von Mengen in Mizar auf einer Menge von Mengen ohne Indexmenge definiert wird. Die entsprechenden Funktoren dazu sind union X (TARSKI:def 4) und meet X (SETFAM_1:def 1), wobei der Schnitt einer leeren Menge wieder als leer definiert wird. Ist dagegen jede Menge in   Teilmenge einer Menge  , X is Subset-Family of D (SETFAM_1), so wird mit Intersection X (SETFAM_1:def 9) der Schnitt der leeren Menge als   definiert (und sonst wie meet X). Keine Referenz für die Beispiele mit  . Die Differenzmenge   ist allgemeiner als X \ Y (XBOOLE_0:def 5) erklärt.

1.1.3.Bearbeiten

Wie im Vorwort erwähnt werden in Fischers Buch Relationen nicht rigoros eingeführt. In Mizar ist eine Abbildung eine spezielle Relation (RELAT_1:def 1). Daher gelten viele offensichtliche Fakten über Abbildungen bereits allgemeiner für Relationen und sind daher in RELAT_1 statt in FUNCT_1 zu finden. Eine Abbildung   ist eine Function (FUNCT_1:def 1).   ist f.x (FUNCT_1:def 2). Eine Abbildung von   nach   ist dann eine Function of X, Y aus FUNCT_2, wobei die wesentlichen Eigenschaften in FUNCT_2:def 1, RELAT_1:def 18,19 eingebaut sind.   ist FUNCT_1:2.   ist Funcs(X,Y) (FUNCT_2:def 2).

Multiplikation reeller Zahlen   ist als a*x definiert in XCMPLX_0:def 5 (und in XREAL_0 passend geclustert),   ist x^2 (SQUARE_1:def 1; für allgemeine Potenzen reeller Zahlen siehe PREPOWER und POWER),   ist sqrt x (SQUARE_1:def 2). Dies sind nur die Vorschriften, die entsprechenden Abbildungen sind a multreal (RVSUM_1:5), sqrreal (RVSUM_1:def 2) und die Wurzeloperation kann dargestellt werden über sqrt id REAL+ (PARTFUN3:def 5, RELAT_1:def 10, ARYTM_2:def 2), keine direkte Referenz.

  ist f.:M (RELAT_1:def 13, FUNCT_1:def 6),   ist f"N (RELAT_1:def 14, FUNCT_1:def 7).   und   sind in RELSET_1 verankert.   ist f"{y} oder Coim(f,y) (RELAT_1:def 17).   ist f | M (RELAT_1:def 11, geclustert in FUNCT_1).

1.1.4.Bearbeiten

injektiv ist one-to-one (FUNCT_1:def 4), surjektiv ist onto (FUNCT_2:def 3), bijektiv ist bijective (FUNCT_2:def 4). Mizar reicht Injektivität, um eine Umkehrabbildung anzugeben:   ist f" (FUNCT_1:def 5, siehe auch RELAT_1:def 7), den passenden Definitions- und Wertebereich liefert FUNCT_2:25.

Der Satz hat keine direkte Referenz, kann aber aus FINSEQ_4:63,64 abgeleitet werden.

1.1.5.Bearbeiten

  ist g * f (RELAT_1:def 8, Reihenfolge des Funktors geändert und geclustert in FUNCT_1), die Anpassung des Definitions- und Wertebereichs erfolgt in RELSET_1.

Bemerkung über die Assoziativität ist RELAT_1:36.

Lemma ist gegeben durch FUNCT_1:39 und FUNCT_2:23, siehe auch FUNCT_1:31 und FUNCT_2:18.

1.1.6.Bearbeiten

Wie zuvor ist auch eine  -Notation für Tupel nicht direkt verfügbar. Ein Paar   kann in Mizar mit der Kuratowski-Definition als [a,b] (TARSKI:def 5) dargestellt werden. Entsprechend gehört zu   [: A, B :] (ZFMISC_1:def 2). Tripel und Quadrupel gibt es als verschachtelte Kuratowski-Paare in XTUPLE_0:def 4,5, wo auch Funktoren definiert werden, um auf die Koordinaten zuzugreifen. Die entsprechenden Produkte aus 3 bzw. 4 Mengen sind dann in ZFMISC_1:def 3,4 definiert. MCART_1 und FUNCT_3 stellen verschiedene Arten der Projektionen bereit.

Eine andere Möglichkeit für die Tupeldarstellung von Elementen einer Menge   ist als abbrechende Folge. Ein Tupel   der Länge   wäre dann einen-element FinSequence of X (CARD_1:def 7 und FINSEQ_1:def 4, siehe außerdem FINSEQ_1:def 2). Dies ist nichts anderes als eine Abbildung   (entsprechend ist   dann x.i), wobei   in Mizar durch Seg n (FINSEQ_1:def 1) gegeben ist. Die Menge aller Tupel über   ist X* (FINSEQ_1:def 11), die Menge aller  -Tupel ist n-tuples_on X (FINSEQ_2:def 4). Funktoren für die direkte Angabe von Tupeln über ihre Koordinaten gibt es für  : FINSEQ_1:def 6 ( ), FINSEQ_1:def 8,9,10 ( ), FINSEQ_4:def 7,8 ( ) und AOFA_A00:def 4,5,6 ( ).

Eine Variante der vorangegangenen Methode ist die Darstellung des Tupels als  , wir beginnen die Zählung also nicht bei   sondern bei  . Ein solches   wäre dann eine n-element XFinSequence of X (AFINSQ_1; man beachte, dass das erste "X" Teil des Bezeichners ist und mit der Variable   nichts zu tun hat). Der Definitionsbereich ist einfach  , da die natürlichen Zahlen so in Mizar definiert wurden (vgl. ORDINAL1). Es gibt nur explizite Funktoren für  : AFINSQ_1:def 2 ( ), AFINSQ_1:def 4,5,6 ( ) und AFINSQ_1:def 14 ( ).

Auf den ersten Blick mag die Tupel-Formalisierung startend mit   aufgrund der vorangegangenen überflüssig erscheinen (gerade da sie erst später der MML hinzugefügt wurde), doch ist sie von Vorteil, wenn man z.B. nicht von vornherein weiß, ob eine vorliegende Folge abbricht oder nicht. AFINSQ_1 enthält auch Sätze, um zwischen den beiden Varianten nach Bedarf zu wechseln. In EXCHSORT werden diese beiden Herangehensweisen in einer Notation generalisiert.

Die vierte Variante formalisiert das allgemeine Produkt von Mengen. Sei   eine beliebige Funktion, die auf Mengen abbildet, dann bezeichnet product f (CARD_3:def 5) die Menge, die alle Funktionen   enthält mit   für alle  . Die Projektionen   sind gegeben durch proj(f,i) (CARD_3:def 16). Falls   und   konstant, degeneriert die vierte zur dritten Variante.

Üblicherweise wird in Beweisen immer die einfachste Variante genommen, die ausreicht.

Eine (unendliche) Folge über   ist eine sequence of X (NAT_1).

1.1.7.Bearbeiten

Aufgrund der Definition einer Funktion als Relation gilt in Mizar  .

1.1.8.Bearbeiten

Relation ist als ihr Graph definiert über RELAT_1:def 1, eine Relation als Teilmenge von   wird in RELSET_1 geclustert. Bei einer Relation   entspricht   dann [a,b] in R. Viele Eigenschaften von Relationen finden sich in RELAT_2.

Eine Menge zusätzlich ausgestattet mit einer Relation ist eine RelStr (ORDERS_2). Sei S eine RelStr, dann wird die dazugehörige Menge mit the carrier of S (s. STRUCT_0) und die dazugehörige Relation mit the InternalRel of S gekennzeichnet. let a, b be Element of S, dann ist   gegeben durch a <= b (ORDERS_2:def 5).

Eine Alternative zu dieser Notation, die ohne struct auskommt, gibt es in ARROW. Dort ist   einer Relation   gegeben durch a <=_R b (ARROW:def 4). Dies wird aber eher selten verwendet.

Beispiele a) Kann man nicht formalisieren.

b) Explizit als Funktor vorhanden:   ist x <= y (XXREAL_0:def 5). Siehe auch die vielen Ungleichungen in XREAL_1.

c) Keine Referenz, aber die Äquivalenzklassen sind die Kreisringe und zu finden als Sphere(x,0) (TOPREAL9:def 3, s. auch EUCLID:def 5).

d) Die Kongruenzrelation ist Cong(m) (INT_4:def 1, s. auch INT_1:def 3,4).

Definition reflexiv ist reflexive (RELAT_2:def 1,9 bzw. ORDERS_2:def 2), symmetrisch ist symmetric (RELAT_2:def 3,11 bzw. NECKLACE:def 3) und transitiv ist transitive (RELAT_2:def 8,16 bzw. ORDERS_2:def 3). Eine Äquivalenzrelation auf   ist eine Equivalence_Relation of X (EQREL_1). Äquivalenzklasse ist kein definierter mode in Mizar, aber die Äquivalenzklasse von   unter   (  im Buch) ist Class(R,x) (in EQREL_1 als Synonym für Im(R,x) (RELAT_1:def 16) eingeführt), die Menge aller Äquivalenzklassen (  im Buch) ist Class R (EQREL_1:def 3). Die angegebenen Eigenschaften sind geclustert in EQREL_1 (1) bzw. EQREL_1:22 (2) und EQREL_1:18,20 (3).

Bemerkung ist EQREL_1:24, siehe auch EQREL_1:def 4 in Verbindung mit EQREL_1:33 (letzteres ist auch ein Nachweis für Eigenschaft (1)  ).

Eine Zerlegung   von   ist a_partition of X (EQREL_1:def 4). Die kanonische Abbildung für eine Zerlegung ist proj P (EQREL_1:def 9).

Aufgaben zu 1.1Bearbeiten

  1. (a) gegeben durch commutativity in XBOOLE_0:def 4,3 (b) XBOOLE_1:16,5 (c) XBOOLE_1:23,24 (d) XBOOLE_1:54,53
  2. (a) RELAT_1:123 und RELAT_1:143 (b) FUNCT_1:76,75 (c) allgemeiner FUNCT_1:69 (d) FUNCT_1:68, RELAT_1:140,120,121; keine Referenz für Gegenbeispiel
  3. (a) FUNCT_1:24, FUNCT_2:27 (b) FUNCT_1:25 und RELAT_1:28
  4. (a) Addition ist definiert in XCMPLX_0:def 4 (und geclustert in XREAL_0),   ist BINOP_2:def 9, keine Referenz für die Eigenschaften (b) keine Referenz (c) keine Referenz
  5. gleichmächtig ist are_equipotent (WELLORD2:def 4, vgl. CARD_1:5), abzählbar unendlich ist denumerable (CARD_3:def 15). (a) TOPGEN_3:16,17 (b) TOPGEN_3:30 with TOPGEN_3:def 4 (c) CARD_2:31 with CARD_1:14
  6. keine Referenz

1.2 GruppenBearbeiten

1.2.1.Bearbeiten

Eine Verknüpfung auf   ist eine BinOp of G (BINOP_1). Einiges zu (b) findet sich in BINOP_2, sonst keine Referenz.

1.2.2.Bearbeiten

Wie die meisten algebraischen Strukturen setzt sich eine Gruppe (Group/addGroup aus GROUP_1/GROUP_1A) in Mizar aus ihren Komponenten zusammen. Die zugrunde liegende Struktur ist multLoopStr /addMagma (ALGSTR_0), also einer Menge, die mit einer Verknüpfung und einer Eins versehen ist (im zweiten Fall wird sie später hinzugefügt). G1 ist associative/add-associative (GROUP_1:def 3/LVECT_1:def 3) und G2 ist Group-like/addGroup-like (GROUP_1:def 2/GROUP_1A:def 2). abelsch ist commutative/Abelian (GROUP_1:def 12/RLVECT_1:def 2).   ist a * b/a + b (ALGSTR_0:def 18/1). Bei einer addGroup wird in Mizar nicht von Kommutativität ausgegangen, ebenso sind die Operatorsymbole fest an die entsprechende Struktur gebunden. Für eine Gruppe   bezeichnet 1_G/0_G (GROUP_1:def 4/GROUP_1A:def 3) das neutrale Element. Für   bezeichnet a"/-a (GROUP_1:def 5/GROUP_1A:def 4) das neutrale Element. addGroup wird nur selten verwendet.

(a) ist SymGroup(X) (CAYLEY:def 2). (b) sind INT.Group (GR_CY_1:def 3), F_Rat (GAUSSINT:def 14) und wahlweise F_Real (VECTSP_1:def 5), G_Real (VECTSP_1:def 1 oder <REAL,+> aus MONOID_0:def 26; keine Referenz für  . (c) keine Referenz.

1.2.3.Bearbeiten

Bemerkung (a,b) Eindeutigkeit steckt in uniqueness von 1_G/0_G bzw. a"/-a;   bzw.   wurde in Group-like/addGroup-like vorgegeben. (c) ist GROUP_1:def 5/GROUP_1A:def 4 (einschließlich involutiveness) und GROUP_1:17/GROUP_1A:16. (d) ist GROUP_1:6/GROUP_1A:6.

1.2.4.Bearbeiten

  ist a*/a+ (TOPGRP_1:def 1/GROUP_1A:def 44) und   ist *a/+a (TOPGRP_1:def 2/GROUP_1A:def 45).

Lemma Bijektivität ist geclustert in TOPGRP_1/GROUP_1A. Keine Referenz für andere Richtung.

1.2.5.Bearbeiten

Keine Referenz für das Tabellenverfahren, aber   ist isomorph zu INT.Group(2/3/4) (GR_CY_1:def 5) bzw. Z/Z(2/3/4) (GROUP_14:def 1; das / in Z/Z ist Teil des Bezeichners), keine Referenz für  .

1.2.6.Bearbeiten

Definition Untergruppe von G ist Subgroup of G (GROUP_2:50-52/GROUP_1A:96-98). Ein Homomorphismus zwischen   und   ist ein Homomorphism of G, H (GROUP_6, s. auch GROUP_6:def 6). Kein spezieller Bezeichner für bijektive Homomorphismen.

Bemerkung 1 steckt in existence von GROUP_2:def 5/GROUP_1A:def 15, die induzierte Verknüpfung ist einfach (the multF of G)||the carrier of H (REALSET1:def 2) (oder entsprechend the addF für addGroup).

Bemerkung 2 (a) GROUP_6:31 (b) GROUP_6:32 (c) GROUP_6:62

Beispiele (a) keine Referenz (b) teilweise indirekt mit SIN_COS:def 23 und SIN_COS:47,50,54 (c) keine Referenz, aber   ist m * INT (MEMBER_1:def 20).

1.2.7.Bearbeiten

  ist r + m * INT (MEMBER_1:def 14). Eine andere Darstellung von 0/1 + 2 * NAT ist EvenNAT/OddNAT (NUMERAL2:def 1/2).   ist a,b are_congruent_mod m (INT_1:def 4), mod can be found in INT_1:def 10. Keine Referenz für die Äquivalenzklassen als ebensolche, aber für   siehe GR_CY_1:def 5 bzw. GROUP_14:def 1, für allgemein Quotientengruppen   siehe G ./. N (GROUP_6:def 4).

Aufgaben zu 1.2Bearbeiten

  1. keine Referenz
  2. keine Referenz
  3. keine Referenz
  4.   ist gr A (GROUP_4:def 4), (i-ii) sind in der MML-Definition enthalten, und die Buchdefinition ist ersichtlich durch GROUP_4:28 in Verbindung mit GROUP_4:def 2 und GROUP_4:def 3.
  5.   entspricht Rotation(1,2,2,2*PI/n) (MATRTOP3:def 3) und   entspricht AxialSymmetry(1,2) (MATRTOP3:def 2). Keine Referenz für   oder die Aufgaben.
  6. zyklisch ist cyclic (GR_CY_1:def 7) (a) keine Referenz (b) GR_CY_2:15,16
  7. s. GROUP_2,3,6, keine Referenz für   in diesem Sinne.
  8. keine Referenz

1.3 Ringe, Körper und PolynomeBearbeiten

1.3.1.Bearbeiten

Definition Ring ist in VECTSP_1 definiert (s. auch RLVECT_1:def 2,3,4, ALGSTR_0:def 11, GROUP_1:def 3, VECTSP_1:def 6,7). Für einen Ring   ist die Null mit 0.R (STRUCT_0:def 6) und die Eins mit 1.R (STRUCT_0:def 7) ausgezeichnet, die Eigenschaft der Eins nach Buch steckt in well-unital (VECTSP_1:def 6). kommutativ ist commutative (GROUP_1:def 12).

Bemerkung ist VECTSP_1:6,7.

Beispiele (a) sind INT.Ring (INT_3:def 3), F_Rat (GAUSSINT:def 14) und F_Real (VECTSP_1:def 5) (b) ist RRing(I) (FUNCSDOM:def 7 und FUNCSDOM:26) (c)   als Ring ist INT.Ring(m) (INT_3:def 12), Synonym Z/m in RING_3 und falls   prim, GF(m) in EC_PF_1.

1.3.2.Bearbeiten

Definition nullteilerfrei ist domRing-like (VECTSP_2:def 1)

Bemerkung Eine Richung ist mit VECTSP_2:1 geclustert in INT_3, die andere Richtung in RING_5.

Definition Teilring ist Subring (C0SP1:def 3), Homomorphismus ist RingHomomorphism (QUOFIELD, s. RINGCAT1:def 1, VECTSP_1:def 20, GROUP_6:def 6, GROUP_1:def 13). Keine Referenz fürs Beispiel, aber vgl. RING_3

1.3.3.Bearbeiten

Definition Ein Körper ist ein Field (VECTSP_1, s. auch STRUCT_0:def 8, VECTSP_1:def 9 und GROUP_1:def 12).

Bemerkung (a) STRUCT_0:def 8 (b) VECTSP_1:6,7 bzw. VECTSP_1:12 (c) VECTSP_1:12 (d) VECTSP_1:8-10 (e) VECTSP_1:5

1.3.4.Bearbeiten

Beispiele für Körper (a) F_Rat (GAUSSINT:def 14) und F_Real (VECTSP_1:def 5) (b) F_Complex (COMPLFLD:def 1, s. unten) (c) GF(2) (mit INT_2:28) (d) geclustert in RING_3

Bemerkung keine Referenz

Definition ist RING_3:def 5

Lemma ist RING_3:86 mit VECTSP_2:1

Komplexe ZahlenBearbeiten

s. hier

1.3.5.Bearbeiten

Wie das Buch schon andeutet, ist das Konzept der Unbekannten mathematisch nicht allzu leicht zu fassen. In der MML wird wie folgt vorgegangen:

In PRE_POLY wird für eine Menge   ein bag of X als eine Funktion von   nach   definiert, die nur an endlich vielen Stellen ungleich Null ist. Ein bag stellt ein Produkt von Potenzen mehrer Unbekannter dar, z.B. entspräche <% 2, 1, 4 %> (AFINSQ_1:def 6, für  ) etwa dem Ausdruck   (oder genauer  ). Die Gesamtheit aller bag of X ist Bags X (PRE_POLY:def 12); Bag 1 entspräche etwa  . Eine formale Potenzreihe über einer Struktur   (z.B. Gruppe, Ring, Körper) ist dann eine Series of X, S (POLYNOM1), was einfach eine Funktion ist, die jedem bag (also Ausdruck wie z.B.  ) einen Koeffizienten in   zuordnet. Etwa ist das konstante Null- bzw. Eins-Polynom 0_(n, S) (POLYNOM1:def 8) bzw. 1_(n, S) (POLYNOM1:def 9), wobei   hier die Anzahl der Variablen darstellt. Ein Polynomial of n, S (POLYNOM1) ist dann eine formale Potenzreihe, in der alle bis auf endlich viele der möglichen Koeffizienten gleich Null sind. POLYNOM3 bietet eine vereinfachte, alternative Notation an, wenn man nur Polynome in einer Variablen braucht: Dort ist ein Polynom einfach eine Funktion von einem Anfangsstück von   auf die Koeffizienten des Polynoms, z.B. entspräche <% 2, 1, 4 %> dem Polynom  . Das Polynomial of S ist einfach ein Synonym in POLYNOM3 für AlgSequence of S (ALGSEQ_1).

  ist Polynom-Ring(1, K) (POLYNOM1:def 11) bzw. Polynom-Ring K (POLYNOM3:def 10).   ist degree f (HURWITZ_2, dort auch als Synonym deg f), wobei abweichend vom Buch   als   definiert ist.   ist Leading-Coefficient(f) (RATFUNC1:def 6, dort auch als Synonym LC(f)), normiert ist normalized (RATFUNC1:def 7). Für   ist   durch eval(f,a) (POLYNOM2:def 4 bzw. POLYNOM4:def 2) gegeben, die Evaluierungsfunktionen durch Polynom-Evaluation(n,K,a) (POLYNOM2:def 5) bzw. Polynom-Evaluation(K,a) (POLYNOM4:def 3).

Beispiel keine Referenz

1.3.6.Bearbeiten

  ist f + g (POLYNOM1:def 6 bzw. geclustert in POLYNOM3; s. auch VFUNCT_1:def 1 bzw. NORMSP_1:def 2).   ist f *' g (POLYNOM1:def 10 bzw. POLYNOM3:def 9).   teilt   ist f divides h (RING_4:def 3 oder HURWITZ:34).

Bemerkung   als kommutativer Ring ist geclustert in POLYNOM1 bzw. POLYNOM3. Die Gradeigenschaft ist HURWITZ:23, die Formalität ist über POLYNOM3:34 geklärt.

1.3.7.Bearbeiten

Satz Existenz und Eindeutigkeit ist in der Definition von f div g (HURWITZ:def 5) gegeben.

Beispiel keine Referenz

1.3.8.Bearbeiten

  ist eine Nullstelle von   ist x is_a_root_of f (POLYNOM5:def 7).

Beispiele (a) keine Referenz (b) keine Referenz

Lemma (1) HURWITZ:33 (s. auch HURWITZ:def 3) (2) HURWITZ:36

Korollar 1 RING_5:22

Korollar 2 keine Referenz

Definition   ist multiplicity(f, x) (UPROOTS:def 8). Die direkte Folgerung ist UPROOTS:52. Keine Referenz für die Beziehung mit den Ableitungen.

1.3.9.Bearbeiten

Keine Referenz für den allgemeinen Fall (  beliebig), aber das Zerfallen eines normierten Polynoms in Linearfaktoren über einem algebraisch geschlossenen Körper ist UPROOTS:65.

Fundamentalsatz der Algebra POLYNOM5:74

Korollar folgt aus UPROOTS:65 und RING_4:23.

1.3.10.Bearbeiten

Lemma keine Referenz

Hilfssatz keine Referenz

Theorem keine Referenz

Korollar keine Referenz

Die Nullstelle eines Polynoms vom Grad 1 ist durch POLYVIE1:9 gegeben. Für die Lösungsformeln für Gleichungen 2. bis 4. Grades siehe POLYEQ_1-5. Keine Referenz für die Unlösbarkeit von Gleichungen fünften Grades oder höher.

1.3.11.Bearbeiten

Keine Referenz für elementarsymmetrische Funktionen.

Vorzeichenregel keine Referenz

Vorzeichenregel von Descartes keine Referenz

Lemma keine Referenz

Aufgaben zu 1.3Bearbeiten

  1. keine Referenz
  2. keine Referenz
  3. keine Referenz
  4. keine Referenz
  5. keine Referenz
  6. keine Referenz
  7. keine Referenz
  8. keine Referenz
  9. keine Referenz
  10. Die Äquivalenzrelation ist implizit über QUOFIELD:def 4 gegeben. Die Addition und Multiplikation sind gegeben durch QUOFIELD:def 6 und QUOFIELD:def 7 bzw. QUOFIELD:def 12 und QUOFIELD:def 13. Der Quotientenring ist gegeben über QUOFIELD:def 16; dass speziell   ein Körper ist, folgt aus den Eigenschaften von   und dem Clustering in QUOFIELD.
  11. keine Referenz
  12. Man kann natürlich einen solchen Beweis in Mizar verfassen, aber zu zeigen, dass dieser die Vorzeichenregel von Descartes sinnvoll nutzt und nicht etwa andere Sätze aus der MML ist nicht formalisierbar (außer durch Formalisierung der Beweise an sich, für die man die gesamte Theorie für die Beweise erneut aufbauen müsste).

1.4 VektorräumeBearbeiten

1.4.1.Bearbeiten

Beispiele (a)   ist n -VectSp_over K (PRVECT_1:def 5).   ist product(the addF of K,n) (PRVECT_1:def 1, s. auch FUNCOP_1:def 3 und FUNCT_3:def 7),   ist n -Mult_over F (PRVECT_1:def 4, s. auch FUNCOP_1:def 5 und FUNCT_3:def 7).

(b) Keine Referenz für  , aber   ist n-Matrices_over K (MATRIX_1:def 1).   ist   (MATRIX_1:def 5),   ist a * A (MATRIX_3:def 5).

(c) Keine Referenz als Funktion  , aber s. BINOP_2:def 5.

(d) S. FVSUM_1:def 6 und Redefinition in POLYNOM1:def 1; bzw. POLYNOM5:def 4.

(e)   ist RealVectSpace(M) (FUNCSDOM:def 6) für   und ComplexVectSpace(M) (CFUNCDOM:def 6) für  , sonst keine Referenz.

Definition Ein  -Vektorraum ist ein VectSp of K (VECTSP_1). Die Menge mit den zwei Verknüpfungen ist eine ModuleStr (VECTSP_1). V1 ist add-associative (RLVECT_1:def 3) right_zeroed (RLVECT_1:def 4) right_complementable (ALGSTR_0:def 16) Abelian (RLVECT_1:def 2) non empty (STRUCT_0:def 1). V2 ist vector-distributive scalar-distributive scalar-associative scalar-unital (VECTSP_1:def 13-16).

Bemerkung (a,b,d) VECTSP_1:14 (c) VECTSP_1:15

1.4.2.Bearbeiten

Definition Ein Untervektorraum von   ist ein Subspace of V (VECTSP_4:def 2, s. auch VECTSP_4:17,20,21 sowie VECTSP_4:34 in Kombination mit VECTSP_4:def 1).

Beispiele (a)   ist (0).V (VECTSP_4:def 3), keine Referenz für die anderen Beispiele.

(b) MATRIX15:def 5

(c)   als Vektorraum ist R_VectorSpace_of_C_0_Functions(REAL) (C0SP2:def 7). Keine Referenz für den Rest.

1.4.3.Bearbeiten

Satz steckt in VECTSP_4:def 2

Lemma Nur definiert für nicht-induzierte Familien:   ist meet M (VECTSP_8:def 5). Spezialfall für zwei Untervektorräume   ist W1 /\ W2 (VECTSP_5:def 2).

Beispiel keine Referenz

Bemerkung VECTSP_5:35

1.4.4.Bearbeiten

Ähnlich wie Polynome ist eine Linearkombination in Mizar definiert als eine Funktion Linear_Combination of V (VECTSP_6:def 1), die jedem Vektor ein Skalar zuordnet und nur endlich vielen ein Skalar ungleich Null. Für eine Linearkombination   wird der dazugehörige Vektor mit Sum f (VECTSP_6:def 6) angegeben. Für eine Teilmenge   von   ist   gegeben durch Lin A (VECTSP_7:def 2).   ist VECTSP_7:9. Keine Referenz für suggestive Notation.

Bemerkung (a) steckt in VECTSP_7:def 2 (b) VECTSP_9:16

Beispiele (a,c,d) keine Referenz (b)   ist Base_FinSeq(n,i) (MATRIXR2:def 4, allgemeiner MATRIX14:def 2), die gesamte Basis ist RN_Base n (EUCLID_7:def 13, dort auch als solche geclustert).

1.4.5.Bearbeiten

Da jede Linearkombination in Mizar implizit alle nicht angegebenen Vektoren mit einem Skalar gleich Null versieht, ist die Linearkombination des Nullvektors mit Nullskalaren in Mizar eindeutig und wird mit ZeroLC(V) (VECTSP_6:def 3) bezeichnet.

Definition Eine linear unabhängige Teilmenge   von   ist linearly-independent (VECTSP_7:def 1); keine Referenz für die Tupel-Definition. Dass die leere Menge linear unabhängig ist, ist in VECTSP_7 geclustert.

Lemma keine Referenz

Beispiele (a) geclustert in EUCLID_7 (b,c) keine Referenz

Bemerkung (a) VECTSP_7:3 (b) VECTSP_7:2 (c) entfällt aufgrund der Mizar-Definition (d) z.T. RANKNULL:21

Aufgaben zu 1.4Bearbeiten

  1. keine Referenz
  2. VECTSP12:def 7
  3. keine Referenz
  4.  -periodisch ist t-periodic (FUNCT_9:def 1); keine Referenz für die Aussagen
  5. keine direkte Referenz, aber s. RSSPACE:def 7,13, RSSPACE3:def 3, LP_SPACE:def 2
  6. keine Referenz
  7. keine Referenz
  8. keine Referenz
  9. keine Referenz
  10. keine Referenz

1.5 Basis und DimensionBearbeiten

1.5.1.Bearbeiten

Definition Keine spezielle Referenz für das Erzeugendensystem. Eine (nicht geordnete) Basis von   ist eine Basis of V (VECTSP_7, s. VECTSP_7:def 3). endlich erzeugt ist finite-dimensional (MATRLIN:def 1). Für eine Basis   ist durch card B (CARD_1:def 2) ihre Länge gegeben. Eine (geordnete) Basis (als Tupel) ist eine OrdBasis of V (MATRLIN:def 2).

Beispiele (a) implizit über VECTSP_7:9 und das Clustering dort (b) geclustert in EUCLID_7 (c,d,e) keine Referenz

1.5.2.Bearbeiten

Satz (i => iv) VECTSP_9:15 (i => ii) implizit in VECTSP_9:14 (sonst) keine Referenz

Zusatz Existenz einer Basis ist geclustert in VECTSP_7, deren Unendlichkeit ergibt sich dann aus der Definition von endlich erzeugt.

1.5.3.Bearbeiten

Basisauswahlsatz VECTSP_7:20, VECTSP_9:20

Theorem geclustert in VECTSP_7

1.5.4.Bearbeiten

Austauschlemma allgemeiner als VECTSP_9:18

Austauschsatz allgemeiner als VECTSP_9:19

1.5.5.Bearbeiten

Korollar 1 implizit über VECTSP_9:20

Korollar 2 uniqueness von VECTSP_9:def 1

Definition   ist dim V (VECTSP_9:def 1), allerdings ohne den unendlichen Fall.

Korollar 3 VECTSP_9:24,25,28

Basisergänzungssatz VECTSP_7:19

Beispiele (a) RLAFFIN3:4 (b) sinngemäß VECTSP_9:30,31 (c,d,e) keine Referenz

1.5.6.Bearbeiten

Mizar hat das Konzept von Anfang an allgemein aufgezogen.

1.5.7.Bearbeiten

Beispiel   ist 1.(K,n) (MATRIX_1:def 3).

  1. Multiplikation der  -ten Zeile mit   ist ScalarXLine(A,i,a) (MATRIX12:def 2)
  2. Addition der  -ten Zeile zur  -ten Zeile ist RlineXScalar(A,i,j,1) (MATRIX12:def 3)
  3. Addition des  -fachen der  -ten Zeile zur  -ten Zeile ist RlineXScalar(A,i,j,a) (MATRIX12:def 3)
  4. Vertauschen der  -ten mit der  -ten Zeile ist InterchangeLine(A,i,j) (MATRIX12:def 1)

Definition Keine spezielle Referenz für  , stattdessen Lin lines A (s. MATRIX13:103 und MATRIX_0:def 7).

Lemma z.T. MATRIX15:69, sonst keine Referenz

Satz keine explizite Referenz, aber s. MATRIX15:sch 1,2

Beispiel keine Referenz

1.5.8.Bearbeiten

  ist A@ (MATRIX_0:def 6); Rechenregeln: (1) MATRIX_6:23 (2) nur reell: MATRIXR1:30 (3) MATRIX_0:57

Definition Mizar definiert den Rang einer Matrix nicht über die Dimension des Zeilen- bzw. Spaltenraums sondern direkt the_rank_of (MATRIX13:def 4) als die Länge der größten squadratischen Submatrix, die aus   durch Löschen von Zeilen und Spalten entstehen kann und Determinante ungleich Null hat.

Lemma implizit über MATRIX13:90,92 bzw. MATRIX13:123

Aufgaben zu 1.5Bearbeiten

  1. keine Referenz
  2. keine Referenz
  3. keine Referenz
  4. keine Referenz
  5. keine Referenz
  6. keine Referenz
  7. keine Referenz
  8. keine Referenz
  9. keine Referenz
  10. keine Referenz
  11. keine Referenz
  12. keine Referenz

1.6 Summen von VektorräumenBearbeiten

1.6.1.Bearbeiten

Definition Nur gegeben für die Summe zweier Vektorräume, W1 + W2 (VECTSP_5:def 1), sonst keine Referenz.

Bemerkung (a) steckt in VECTSP_5:def 1 (b) implizit durch VECTSP_7:15 und VECTSP_7:11 (c) implizit durch VECTSP_9:32

Dimensionsformel für Summen VECTSP_9:32

1.6.2.Bearbeiten

Lemma keine Referenz

Definition   ist V is_the_direct_sum_of W1, W2 (VECTSP_5:def 4).

1.6.3.Bearbeiten

Satz (i => ii) implizit durch VECTSP12:9 (i => iii) VECTSP_5:def 4, VECTSP_9:34 (sonst) keine Referenz

Korollar   ist Linear_Compl of V (VECTSP_5:def 5)

1.6.4.Bearbeiten

Definition keine Referenz

Beispiel keine Referenz

Satz keine Referenz

Aufgaben zu 1.6Bearbeiten

  1. keine Referenz
  2. keine Referenz
  3.   ist (schief)symmetrisch ist A is (anti)symmetric (MATRIX_6:def 5,6); keine Referenz für die Aufgaben