Volume 16 (2008): Issue 1 (March 2008)

For each set X, the power set of X forms a vector space over the field Z2 (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 · x:= x, 0 · x := ∅ for subsets x of X). See [10], Exercise 2.K, for more information.

MML identifier: BSPACE, version: 7.8.05 4.89.993

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 [11]. The proof given here is based on Poincaré's linear algebraic proof, stated in [17] (with a corrected proof in [18]), as adapted by Imre Lakatos in the latter's Proofs and Refutations [15].

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).

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.

The main theorem, expressed in the language of the present article, is

Sum alternating - characteristic - sequence (p) = 0,

where p is a polyhedron. The alternating characteristic sequence of a polyhedron is the sequence

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.)

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.

A treatment of the more general version of Euler's relation can be found in [12] and [6]. The former contains a proof of Steinitz's theorem, which shows that the abstract polyhedra treated in Poincaré's proof, which might not appear to be about polyhedra in the usual sense of the word, are in fact embeddable in R³ under certain conditions. It would be valuable to formalize a proof of Steinitz's theorem and relate it to the development contained here.

MML identifier: POLYFORM, version: 7.8.05 4.89.993

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) [20], [9], [3], quoted it and proved the uniform boundedness principle. Moreover, the proof of the Banach-Steinhaus theorem is added.

MML identifier: LOPBAN 5, version: 7.8.05 4.89.993

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 [14], [12]. Finally, Gauss Lemma and Law of Quadratic Reciprocity are proven.

MML identifier: INT 5, version: 7.8.05 4.89.993

This is the second article on regular expression quantifiers. [4] 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 [8], several properties of regular expressions from [7].

MML identifier: FLANG 3, version: 7.8.05 4.89.993

This paper is a continuation of [12]. 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 [13].

MML identifier: COMPL SP, version: 7.8.05 4.89.993

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 [11].

MML identifier: DIFF 2, version: 7.8.09 4.97.1001

In this article, we prove the first mean value theorem for integrals [16]. The formalization of various theorems about the properties of the Lebesgue integral is also presented.

MML identifier: MESFUNC7, version: 7.8.09 4.97.1001

The goal of this article is to prove Egoroff's Theorem [13]. 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.

MML identifier: MESFUNC8, version: 7.8.10 4.100.1011

In this article we will first investigate the elementary properties of BCI-algebras with condition (S), see [8]. And then we will discuss the three classes of algebras: commutative, positive-implicative and implicative BCK-algebras with condition (S).

MML identifier: BCIALG 4, version: 7.8.09 4.97.1001

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.

MML identifier: GFACIRC2, version: 7.8.09 4.97.1001

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.

MML identifier: MATRIX15, version: 7.8.09 4.97.1001