# Volume 21 (2013): Issue 2 (June 2013)

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

0 Articles
Open Access

#### N-Dimensional Binary Vector Spaces

Published Online: 01 Jun 2013
Page range: 75 - 81

#### Abstract

The binary set {0, 1} together with modulo-2 addition and multiplication is called a binary field, which is denoted by F2. The binary field F2 is defined in . A vector space over F2 is called a binary vector space. The set of all binary vectors of length n forms an n-dimensional vector space Vn over F2. Binary fields and n-dimensional binary vector spaces play an important role in practical computer science, for example, coding theory  and cryptology. In cryptology, binary fields and n-dimensional binary vector spaces are very important in proving the security of cryptographic systems . In this article we define the n-dimensional binary vector space Vn. Moreover, we formalize some facts about the n-dimensional binary vector space Vn.

#### Keywords

• formalization of binary vector space
Open Access

#### Some Properties of the Sorgenfrey Line and the Sorgenfrey Plane

Published Online: 01 Jun 2013
Page range: 83 - 85

#### Abstract

We first provide a modified version of the proof in  that the Sorgenfrey line is T1. Here, we prove that it is in fact T2, a stronger result. Next, we prove that all subspaces of ℝ1 (that is the real line with the usual topology) are Lindel¨of. We utilize this result in the proof that the Sorgenfrey line is Lindel¨of, which is based on the proof found in . Next, we construct the Sorgenfrey plane, as the product topology of the Sorgenfrey line and itself. We prove that the Sorgenfrey plane is not Lindel¨of, and therefore the product space of two Lindel¨of spaces need not be Lindel¨of. Further, we note that the Sorgenfrey line is regular, following from :59. Next, we observe that the Sorgenfrey line is normal since it is both regular and Lindel¨of. Finally, we prove that the Sorgenfrey plane is not normal, and hence the product of two normal spaces need not be normal. The proof that the Sorgenfrey plane is not normal and many of the lemmas leading up to this result are modelled after the proof in , that the Niemytzki plane is not normal. Information was also gathered from .

#### Keywords

• topological spaces
• products of normal spaces
• Sorgenfrey line
• Sorgenfrey plane
• Lindelöf spaces
Open Access

#### More on Divisibility Criteria for Selected Primes

Published Online: 01 Jun 2013
Page range: 87 - 94

#### Abstract

This paper is a continuation of , where the divisibility criteria for initial prime numbers based on their representation in the decimal system were formalized. In the current paper we consider all primes up to 101 to demonstrate the method presented in .

#### Keywords

• divisibility
• divisibility rules
• decimal digits
Open Access

#### Differentiation in Normed Spaces

Published Online: 01 Jun 2013
Page range: 95 - 102

#### Abstract

In this article we formalized the Fréchet differentiation. It is defined as a generalization of the differentiation of a real-valued function of a single real variable to more general functions whose domain and range are subsets of normed spaces .

#### Keywords

• formalization of Fréchet derivative
• Fréchet differentiability
Open Access

#### Polygonal Numbers

Published Online: 01 Jun 2013
Page range: 103 - 113

#### Abstract

In the article the formal characterization of triangular numbers (famous from  and words “EYPHKA! num = Δ+Δ+Δ”)  is given. Our primary aim was to formalize one of the items (#42) from Wiedijk’s Top 100 Mathematical Theorems list , namely that the sequence of sums of reciprocals of triangular numbers converges to 2. This Mizar representation was written in 2007. As the Mizar language evolved and attributes with arguments were implemented, we decided to extend these lines and we characterized polygonal numbers. We formalized centered polygonal numbers, the connection between triangular and square numbers, and also some equalities involving Mersenne primes and perfect numbers. We gave also explicit formula to obtain from the polygonal number its ordinal index. Also selected congruences modulo 10 were enumerated. Our work basically covers the Wikipedia item for triangular numbers and the Online Encyclopedia of Integer Sequences (http://oeis.org/A000217). An interesting related result  could be the proof of Lagrange’s four-square theorem or Fermat’s polygonal number theorem .

#### Keywords

• triangular number
• polygonal number
• reciprocals of triangular numbers
Open Access

#### Gaussian Integers

Published Online: 01 Jun 2013
Page range: 115 - 125

#### Abstract

Gaussian integer is one of basic algebraic integers. In this article we formalize some definitions about Gaussian integers . We also formalize ring (called Gaussian integer ring), Z-module and Z-algebra generated by Gaussian integer mentioned above. Moreover, we formalize some definitions about Gaussian rational numbers and Gaussian rational number field. Then we prove that the Gaussian rational number field and a quotient field of the Gaussian integer ring are isomorphic.

#### Keywords

• formalization of Gaussian integers
• algebraic integers
Open Access

#### Commutativeness of Fundamental Groups of Topological Groups

Published Online: 01 Jun 2013
Page range: 127 - 131

#### Abstract

In this article we prove that fundamental groups based at the unit point of topological groups are commutative .

#### Keywords

• fundamental group
• topological group
Open Access

#### Constructing Binary Huffman Tree

Published Online: 01 Jun 2013
Page range: 133 - 143

#### Abstract

Huffman coding is one of a most famous entropy encoding methods for lossless data compression . JPEG and ZIP formats employ variants of Huffman encoding as lossless compression algorithms. Huffman coding is a bijective map from source letters into leaves of the Huffman tree constructed by the algorithm. In this article we formalize an algorithm constructing a binary code tree, Huffman tree.

#### Keywords

• formalization of Huffman coding tree
• source coding
Open Access

#### Riemann Integral of Functions from ℝ into Real Banach Space

Published Online: 01 Jun 2013
Page range: 145 - 152

#### Abstract

In this article we deal with the Riemann integral of functions from R into a real Banach space. The last theorem establishes the integrability of continuous functions on the closed interval of reals. To prove the integrability we defined uniform continuity for functions from R into a real normed space, and proved related theorems. We also stated some properties of finite sequences of elements of a real normed space and finite sequences of real numbers. In addition we proved some theorems about the convergence of sequences. We applied definitions introduced in the previous article  to the proof of integrability.

#### Keywords

• formalization of Riemann integral
Open Access

#### On Square-Free Numbers

Published Online: 01 Jun 2013
Page range: 153 - 162

#### Abstract

In the article the formal characterization of square-free numbers is shown; in this manner the paper is the continuation of . Essentially, we prepared some lemmas for convenient work with numbers (including the proof that the sequence of prime reciprocals diverges ) according to  which were absent in the Mizar Mathematical Library. Some of them were expressed in terms of clusters’ registrations, enabling automatization machinery available in the Mizar system. Our main result of the article is in the final section; we proved that the lattice of positive divisors of a positive integer n is Boolean if and only if n is square-free.

#### Keywords

• square-free numbers
• prime reciprocals
• lattice of natural divisors