- Journal Details
- Format
- Journal
- eISSN
- 1898-9934
- ISSN
- 1426-2630
- First Published
- 09 Jun 2008
- Publication timeframe
- 4 times per year
- Languages
- English

#### Search

Open Access

#### The Vector Space of Subsets of a Set Based on Symmetric Difference

Page range: 1 - 5

#### Abstract

For each set

MML identifier: BSPACE, version: 7.8.05 4.89.993

#### Abstract

Euler's polyhedron theorem states for a polyhedron

where

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

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

Sum alternating - characteristic - sequence (

where

where

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 ^{3} 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

#### Abstract

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

Open Access

#### Gauss Lemma and Law of Quadratic Reciprocity

Page range: 23 - 28

#### Abstract

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

Open Access

#### Regular Expression Quantifiers - at least m Occurrences

Page range: 29 - 33

#### Abstract

This is the second article on regular expression quantifiers. [4] introduced the quantifiers

MML identifier: FLANG 3, version: 7.8.05 4.89.993

#### Abstract

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

Open Access

#### Difference and Difference Quotient. Part II

Page range: 45 - 49

#### Abstract

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

Open Access

#### The First Mean Value Theorem for Integrals

Page range: 51 - 55

#### Abstract

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

#### Abstract

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

Open Access

#### BCI-algebras with Condition (S) and their Properties

Page range: 65 - 71

#### Abstract

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

Open Access

#### Stability of n -Bit Generalized Full Adder Circuits (GFAs). Part II

Page range: 73 - 80

#### Abstract

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

MML identifier: GFACIRC2, version: 7.8.09 4.97.1001

#### Abstract

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