A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Jesse Alama.
The Vector Space of Subsets of a
Set Based on Symmetric Difference,
Formalized Mathematics 16(1),
pages 1-5, 2008. MML Identifier:
BSPACE Summary:
For each set $X$, the power set of $X$ forms a vector space over the
field ${\bf Z}_{2}$ (the two-element field $\{0,1\}$ with addition and
multiplication done modulo $2$): vector addition is disjoint union,
and scalar multiplication is defined by the two equations
($1 \cdot x := x$, $0 \cdot x := \emptyset$ for subsets $x$ of $X$).
See \cite{kelley},
Exercise 2.K, for more information.
Jesse Alama.
Euler's Polyhedron Formula,
Formalized Mathematics 16(1),
pages 7-17, 2008. MML Identifier:
POLYFORM Summary:
Euler's polyhedron theorem states for a polyhedron $p$,
that $$ V - E + F = 2, $$ where $V$, $E$, and $F$ are,
respectively, the number of vertices, edges, and faces of $p$.
The formula was first stated in print by Euler in 1758
\cite{euler1758a}.
The proof given here is based on Poincar\'e's linear algebraic proof,
stated in \cite{poincare1893}
(with a corrected proof
in \cite{poincare1899}),
as adapted by Imre Lakatos in the
latter's \textsl{Proofs and Refutations}
\cite{proofs-and-refutations}.
\par As
is well known, Euler's formula is not true for all polyhedra.
The condition on polyhedra considered here is that of being a homology sphere,
which says that the cycles (chains whose boundary is zero) are
exactly the bounding chains (chains that are the boundary of
a chain of one higher dimension).\par The present proof actually
goes beyond the three-dimensional version of the polyhedral formula
given by Lakatos; it is dimension-free, in the sense that it gives a
formula in which the dimension of the polyhedron is a parameter.
The classical Euler relation $V - E + F = 2$ is corresponds to the
case where the dimension of the polyhedron is $3$. \par The main
theorem, expressed in the language of the present article,
is $$\mathtt{Sum \ alternating-characteristic-sequence(p) = 0},$$
where $p$ is a polyhedron. The alternating characteristic sequence
of a polyhedron is the sequence $$ -N(-1), +N(0), -N(1), \dots,
(-1)^{\dim(p)}*N(\dim(p)),$$
where $N(k)$ is the number of polytopes of $p$ of dimension $k$.
The special case of $\dim(p) = 3$ yields Euler's classical
relation. ($N(-1)$ and $N(3)$ will turn out to be equal, by definition,
to $1$.) \par Two other special cases are proved:
the first says that a one-dimensional ``polyhedron" that is a homology sphere
consists of just two vertices (and thus consists of just a single edge);
the second special case asserts that a two-dimensional
polyhedron that is a homology sphere (a polygon) has as many vertices as edges.
\par A treatment of
the more general version of Euler's relation can be found in
\cite{grunbaum2003}
and \cite{brondsted1983}.
The former contains a proof of Steinitz's theorem,
which shows that the abstract polyhedra treated in Poincar\'e's proof,
which might not appear to be about polyhedra in the usual sense of the word,
are in fact embeddable in $\mathbf{R}^3$ under certain conditions. It would
be valuable to formalize a proof of Steinitz's theorem and relate it to the
development contained here.
Hideki Sakurai, Hisayoshi Kunimune, Yasunari Shidama.
Uniform Boundedness Principle,
Formalized Mathematics 16(1),
pages 19-21, 2008. MML Identifier:
LOPBAN_5 Summary:
In this article at first, we proved the lemma of the inferior limit
and the superior limit. Next, we proved the Baire category theorem
(Banach space version)
\cite{yoshida:1980},
\cite{miyadera:1972},
\cite{Dunford:1958},
quoted it and proved the uniform boundedness
principle. Moreover, the proof of the Banach-Steinhaus theorem is added.
Li Yan, Xiquan Liang, Junjie Zhao.
Gauss Lemma and Law of Quadratic Reciprocity,
Formalized Mathematics 16(1),
pages 23-28, 2008. MML Identifier:
INT_5 Summary:
In this paper, we defined the quadratic residue and proved its
fundamental properties on the base of some useful theorems.
Then we defined the Legendre symbol and proved its useful theorems
\cite{HuaLooKeng:1957},
\cite{Dexin:1965}. Finally, Gauss Lemma and
Law of Quadratic Reciprocity are proven.
Micha{\l} Trybulec.
Regular Expression Quantifiers -- at least $m$ Occurrences,
Formalized Mathematics 16(1),
pages 29-33, 2008. MML Identifier:
FLANG_3 Summary:
This is the second article on regular expression quantifiers.
\cite{FLANG_2.ABS}
introduced the quantifiers $m$ to $n$ occurrences
and optional occurrence. In the sequel, the quantifiers: at least $m$
occurrences and positive closure (at least 1 occurrence) are introduced.
Notation and terminology were taken from
\cite{WALL-CHRISTIANSEN-ORWANT:2000},
several properties of regular expressions from
\cite{WAITE-GOOS:1984}.
Karol P\k{a}k.
Complete Spaces,
Formalized Mathematics 16(1),
pages 35-43, 2008. MML Identifier:
COMPL_SP Summary:
This paper is a continuation of
\cite{TBSP_1.ABS}.
First some definitions needed to formulate Cantor's theorem on
complete spaces and show several facts about them are introduced.
Next section contains the proof of Cantor's theorem and some properties
of complete spaces resulting from this theorem. Moreover,
countable compact spaces and proofs of auxiliary facts about them
is defined. I also show the important condition that every metric space
is compact if and only if it is countably compact. Then I prove that
every metric space is compact if and only if it is a complete and totally
bounded space. I also introduce the definition of the metric space with
the well metric. This article is based on
\cite{ENGEL:1}.
Bo Li, Yanping Zhuang, Xiquan Liang.
Difference and Difference Quotient. {P}art {II},
Formalized Mathematics 16(1),
pages 45-49, 2008. MML Identifier:
DIFF_2 Summary:
In this article, we give some important properties of forward
difference, backward difference, central difference and difference
quotient and forward difference, backward difference, central
difference and difference quotient formulas of some special functions
\cite{Renhong:1999}.
Keiko Narita, Noboru Endou, Yasunari Shidama.
The First Mean Value Theorem for Integrals,
Formalized Mathematics 16(1),
pages 51-55, 2008. MML Identifier:
MESFUNC7 Summary:
In this article, we prove the first mean value theorem for integrals
\cite{Halmos74}.
The formalization of various theorems about the properties
of the Lebesgue integral is also presented.
Noboru Endou, Yasunari Shidama, Keiko Narita.
Egoroff's Theorem,
Formalized Mathematics 16(1),
pages 57-63, 2008. MML Identifier:
MESFUNC8 Summary:
The goal of this article is to prove Egoroff's Theorem
\cite{Halmos74}.
However, there are not enough theorems related to sequence of measurable functions in
Mizar Mathematical Library.
So we proved many theorems about them. At the end of this article, we showed Egoroff's theorem.
Tao Sun, Junjie Zhao, Xiquan Liang.
BCI-algebras with Condition ({S})
and their Properties,
Formalized Mathematics 16(1),
pages 65-71, 2008. MML Identifier:
BCIALG_4 Summary:
In this article we will first investigate the elementary properties of
BCI-algebras with condition (S), see
\cite{BCIAlgebras}.
And then we will discuss the three classes of algebras:
commutative, positive-implicative and implicative BCK-algebras
with condition (S).
Katsumi Wasaki.
Stability of $n$-Bit Generalized Full
Adder Circuits ({GFA}s). {P}art {II},
Formalized Mathematics 16(1),
pages 73-80, 2008. MML Identifier:
GFACIRC2 Summary:
We continue to formalize the concept of the Generalized Full
Addition and Subtraction circuits (GFAs), define the structures of
calculation units for the Redundant Signed Digit (RSD) operations,
then prove its stability of the calculations. Generally, one-bit
binary full adder assumes positive weights to all of its three binary
inputs and two outputs. We define the circuit structure of
two-types $n$-bit GFAs using the recursive construction to use the
RSD arithmetic logical units that we generalize full adder to have
both positive and negative weights to inputs and outputs.
The motivation for this research is to establish a technique
based on formalized mathematics and its applications for
calculation circuits with high reliability.
Karol P\k{a}k.
Solutions of Linear Equations,
Formalized Mathematics 16(1),
pages 81-90, 2008. MML Identifier:
MATRIX15 Summary:
In this paper I present the Kronecker-Capelli theorem which states
that a system of linear equations has a solution if and only if
the rank of its coefficient matrix is equal to the rank of its augmented matrix.