First commit

Signed-off-by: David A. Wheeler <[email protected]>

Author: david-a-wheeler

Diff for: README.TXT

@@ -0,0 +1,86 @@
+This is the REAME.TXT file that accompanies the Metamath site download,
+extracted from one of the downloaded files metamathsite.tar.bz2,
+metamathsite.tar.gz, or metamathsite.zip.
+
+This package contains the minimal sources and other files needed to
+rebuild the Metamath site from scratch.  It is not usable until you run
+the bash script "install.sh" (see below).  You will need around 650MB of
+free disk space.
+
+
+
+How to build the Metamath site
+------------------------------
+
+To use the script install.sh to build the Metamath site, you will need
+a Unix or Unix-like system (such as Cygwin for Windows) that includes
+a bash shell.
+
+
+
+A. The simple way to do it
+--------------------------
+
+To build the Metamath web site from a bash shell, type
+
+  ./install.sh
+
+in the metamathsite (i.e. this) directory.  During the installation, a
+lot of status messages will flash by on the screen.  When done, the last
+line on the screen should read:
+
+  The installation completed successfully.  The home page is index.html.
+
+
+
+B. A more cautious way to do it
+--------------------------------
+
+To build the Metamath web site from a bash shell, type
+
+   sh -x ./install.sh >install.log 2>&1
+
+You can monitor the progress in another bash shell window with "tail -f
+install.log".  The last line in install.log should read:
+
+  The installation completed successfully.  The home page is index.html.
+
+After the installation is completed, check the install.log file for
+problems:
+
+  egrep -i \
+    "warning|error|no such|cannot|permission|denied|invalid|too long|can't" \
+      install.log | egrep -v \
+    "No errors|Font Warn|label token|ignored|may have changed"
+
+If all went OK there should be no output.
+
+
+
+Notes
+-----
+
+1. The script install.sh is the actual script used to rebuild this site
+periodically.  In the hopefully unlikely event there is a problem,
+please report it to Norm Megill - this is important to help maintain the
+quality of the Metamath site!  There are also some additional notes in
+the comments at the beginning of the install.sh file.
+
+2. To conserve about 70MB of disk space on a personal local copy (not a
+mirror site!), after the installation you can remove the redundant
+download files:
+
+  rm downloads/m?[a-ik-z]*z* downloads/ql* downloads/s*
+
+
+=======================================================================
+
+Copyright
+---------
+
+See the file copyright.html in this directory for copyright and
+licensing information that applies to the content of this package.  The
+file is also at http://us.metamath.org/copyright.html on the web.
+
+
+Norm Megill  nm(at)alum(dot)mit(dot)edu  10-Dec-2006

Diff for: __README.TXT

@@ -0,0 +1,86 @@
+This is the REAME.TXT file that accompanies the Metamath site download,-e 
+extracted from one of the downloaded files metamathsite.tar.bz2,-e 
+metamathsite.tar.gz, or metamathsite.zip.-e 
+-e 
+This package contains the minimal sources and other files needed to-e 
+rebuild the Metamath site from scratch.  It is not usable until you run-e 
+the bash script "install.sh" (see below).  You will need around 650MB of-e 
+free disk space.-e 
+-e 
+-e 
+-e 
+How to build the Metamath site-e 
+-------------------------------e 
+-e 
+To use the script install.sh to build the Metamath site, you will need-e 
+a Unix or Unix-like system (such as Cygwin for Windows) that includes-e 
+a bash shell.-e 
+-e 
+-e 
+-e 
+A. The simple way to do it-e 
+---------------------------e 
+-e 
+To build the Metamath web site from a bash shell, type-e 
+-e 
+  ./install.sh-e 
+-e 
+in the metamathsite (i.e. this) directory.  During the installation, a-e 
+lot of status messages will flash by on the screen.  When done, the last-e 
+line on the screen should read:-e 
+-e 
+  The installation completed successfully.  The home page is index.html.-e 
+-e 
+-e 
+-e 
+B. A more cautious way to do it-e 
+---------------------------------e 
+-e 
+To build the Metamath web site from a bash shell, type-e 
+-e 
+   sh -x ./install.sh >install.log 2>&1-e 
+-e 
+You can monitor the progress in another bash shell window with "tail -f-e 
+install.log".  The last line in install.log should read:-e 
+-e 
+  The installation completed successfully.  The home page is index.html.-e 
+-e 
+After the installation is completed, check the install.log file for-e 
+problems:-e 
+-e 
+  egrep -i \-e 
+    "warning|error|no such|cannot|permission|denied|invalid|too long|can't" \-e 
+      install.log | egrep -v \-e 
+    "No errors|Font Warn|label token|ignored|may have changed"-e 
+-e 
+If all went OK there should be no output.-e 
+-e 
+-e 
+-e 
+Notes-e 
+------e 
+-e 
+1. The script install.sh is the actual script used to rebuild this site-e 
+periodically.  In the hopefully unlikely event there is a problem,-e 
+please report it to Norm Megill - this is important to help maintain the-e 
+quality of the Metamath site!  There are also some additional notes in-e 
+the comments at the beginning of the install.sh file.-e 
+-e 
+2. To conserve about 70MB of disk space on a personal local copy (not a-e 
+mirror site!), after the installation you can remove the redundant-e 
+download files:-e 
+-e 
+  rm downloads/m?[a-ik-z]*z* downloads/ql* downloads/s*-e 
+-e 
+-e 
+=======================================================================-e 
+-e 
+Copyright-e 
+----------e 
+-e 
+See the file copyright.html in this directory for copyright and-e 
+licensing information that applies to the content of this package.  The-e 
+file is also at http://us.metamath.org/copyright.html on the web.-e 
+-e 
+-e 
+Norm Megill  nm(at)alum(dot)mit(dot)edu  10-Dec-2006-e 

Diff for: _award_jars.gif

@@ -0,0 +1,93 @@
+<!doctype html public "-//w3c//dtd html 4.0 transitional//en">
+<html>
+<head>
+<BASE HREF="http://www.math.ucdavis.edu/~suh/abian/abian-themostfixed.html">
+
+   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+   <meta name="GENERATOR" content="Mozilla/4.77 [en] (WinNT; U) [Netscape]">
+   <title> A  MOST  FUNDAMENTAL  FIXED  POINT  THEOREM  </title>
+</head>
+<body bgcolor="#FFFFFF">
+<I><FONT COLOR=green>(Note: This is a copy of a page from
+ Alexander Abian's web site circa 1999. - N. Megill 11-Jun-2009)</FONT></I>
+&nbsp;
+<center>
+<h2>
+A MOST FUNDAMENTAL FIXED POINT THEOREM&nbsp;<br>
+<br>
+<b>Alexander Abian</b></h2></center>
+
+<p><br><DOUBLE>&nbsp; The following a most Fundamental Fixed Point Theorem
+is proved in&nbsp;&nbsp; ZF&nbsp;&nbsp; set theory
+<p><b>without the Axiom of Choice.</b>&nbsp; It is "<b> a most fundamental</b>"
+in the sense that it gives a
+<p>necessary and sufficient condition for the existence of a fixed point
+of a mapping of a set&nbsp;&nbsp; S
+<p>into itself where absolutely no algebraic or analytic or order theoretic
+or any other special
+<p>structures are imposed on&nbsp;&nbsp; S.
+<p>&nbsp; <b>THEOREM</b> (<b>Abian</b>). Let&nbsp;&nbsp; f&nbsp;&nbsp;
+be a mapping from a set S into itself. Then&nbsp;&nbsp; f&nbsp;&nbsp; has
+a fixed point if
+<p>and only if:
+<br>&nbsp; There exists an element&nbsp;&nbsp; a&nbsp;&nbsp; of&nbsp;&nbsp;
+P&nbsp;&nbsp; such that&nbsp;&nbsp; f<sup>k</sup>(a)&nbsp;&nbsp; is an
+element of&nbsp;&nbsp; P&nbsp;&nbsp; for every ordinal&nbsp;&nbsp; k,&nbsp;&nbsp;
+and
+<br>for every ordinal&nbsp;&nbsp; v
+<p>(1)&nbsp;&nbsp; if&nbsp;&nbsp; f<sup>v</sup>(a)&nbsp;&nbsp; is not a
+fixed point of&nbsp;&nbsp; f&nbsp;&nbsp; then&nbsp; the&nbsp;&nbsp; f<sup>u</sup>(a)
+'s are all distinct for every ordinal&nbsp; u&nbsp; &lt; v.
+<p>&nbsp; <b>PROOF.</b>&nbsp; First we show that (1) implies that&nbsp;&nbsp;
+f&nbsp;&nbsp; has a fixed point.&nbsp; Assume on the contrary that&nbsp;&nbsp;
+f
+<p>&nbsp; has no fixed point and let&nbsp;&nbsp; p&nbsp;&nbsp; and&nbsp;&nbsp;
+q&nbsp;&nbsp; be any two distinct ordinal numbers.&nbsp; Clearly, there
+always
+<p>exists an ordinal&nbsp;&nbsp; v&nbsp;&nbsp; such that&nbsp;&nbsp;&nbsp;&nbsp;
+p &lt; v&nbsp;&nbsp; and&nbsp;&nbsp; q &lt; v.&nbsp;&nbsp;&nbsp; But then
+since by our assumption&nbsp;&nbsp; f<sup>v</sup>(a)
+<p>cannot be a fixed point of&nbsp;&nbsp; f&nbsp;&nbsp; hence (1) implies
+that&nbsp;&nbsp; f<sup>p</sup>(a)&nbsp;&nbsp; and&nbsp;&nbsp; f<sup>q</sup>(a)&nbsp;&nbsp;
+are two distinct elements
+<p>of&nbsp;&nbsp; S.&nbsp; Thus, our assumption implies that for every
+two distinct ordinals&nbsp;&nbsp; p&nbsp;&nbsp; and&nbsp;&nbsp; q&nbsp;&nbsp;
+there
+<p>correspond two distinct elements&nbsp;&nbsp; f<sup>p</sup>(a)&nbsp;&nbsp;
+and&nbsp;&nbsp; f<sup>q</sup>(a)&nbsp;&nbsp; of the set&nbsp;&nbsp; S.&nbsp;
+Consequently, every ordinal can
+<p>be assigned in a one-to-one way to every element of a subset of&nbsp;&nbsp;
+S.&nbsp; But then the Axiom Scheme
+<p>of Replacement of&nbsp;&nbsp; ZF&nbsp;&nbsp; would imply that the set
+of all ordinals exists, which is a contradiction.
+<p>Thus, our assumption is false and&nbsp;&nbsp; f&nbsp;&nbsp; has a fixed
+point.
+<p>&nbsp; Next, assume that&nbsp;&nbsp; f&nbsp;&nbsp; has a fixed point&nbsp;&nbsp;
+a.&nbsp; Then&nbsp; (1 ) is obviously satisfied by setting
+<p>a = f(a) = f<sup>k</sup>(a)&nbsp;&nbsp; for every ordinal&nbsp;&nbsp;
+k.
+<p>&nbsp; Thus,&nbsp; the Theorem is proved.
+<p>&nbsp; <b>REMARK.</b>&nbsp; Note that&nbsp;&nbsp; f<sup>k</sup>(a)&nbsp;&nbsp;
+in the above does not necessarily indicate the k-th or any other
+<p>iterates of&nbsp;&nbsp; f.&nbsp; Thus, it is not even required that&nbsp;
+f(f<sup>k</sup>(a))&nbsp;&nbsp; be equal to&nbsp;&nbsp; f<sup>k+1</sup>(a).&nbsp;&nbsp;
+Obviously, by
+<p>"&nbsp; f<sup>k</sup>(a)&nbsp; is a fixed point of&nbsp;&nbsp; f&nbsp;
+"&nbsp;&nbsp; is meant that&nbsp;&nbsp; f(f<sup>k</sup>(a))&nbsp;&nbsp;
+=&nbsp;&nbsp; f<sup>k</sup>(a),&nbsp; and as mentioned above,
+<p>without necessitating that&nbsp;&nbsp; f(f<sup>k</sup>(a))&nbsp;&nbsp;
+be equal to&nbsp;&nbsp; f<sup>k+1</sup>(a).
+<p>&nbsp; The fundamental significance of the Theorem lies in the fact
+that a great many fixed point
+<p>theorems can be reduced to the special cases of the Theorem, in as much
+as, no special structures
+<p>are required by the set&nbsp;&nbsp; S&nbsp;&nbsp; to have, and, no iterative
+rules are imposed on&nbsp;&nbsp; f.
+<p><b><a href="http://www.math.iastate.edu/abian/">Alexander Abian</a></b>
+<br>Dept .of Math. Iowa state Univ.
+<br>Ames, IA, 50011, USA.
+<br><b>e-mail:</b> <a href="mailto:[email protected]"><b>abian</b>@iastate.edu</a>
+<br>&nbsp;
+</body>
+
+</html>