Volume 26 (2018): Issue 3 (October 2018)

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

Arithmetic Operations on Short Finite Sequences

Published Online: 23 Feb 2019
Page range: 199 - 208

Abstract

In contrast to other proving systems Mizar Mathematical Library, considered as one of the largest formal mathematical libraries [4], is maintained as a single base of theorems, which allows the users to benefit from earlier formalized items [3], [2]. This eventually leads to a development of certain branches of articles using common notation and ideas. Such formalism for finite sequences has been developed since 1989 [1] and further developed despite of the controversy over indexing which excludes zero [6], also for some advanced and new mathematics [5].

The article aims to add some new machinery for dealing with finite sequences, especially those of short length.

Keywords

• finite sequences
• functions
• relations

MSC 2010

• 11B99
• 03B35
• 68T99
Open Access

Published Online: 23 Feb 2019
Page range: 209 - 222

Abstract

This article covers some technical aspects about the product topology which are usually not given much of a thought in mathematics and standard literature like [7] and [6], not even by Bourbaki in [4].

Let {Ti}i∈I be a family of topological spaces. The prebasis of the product space T = ∏i∈I Ti is defined in [5] as the set of all π−1i(V) with i ∈ I and V open in Ti. Here it is shown that the basis generated by this prebasis consists exactly of the sets ∏i∈I Vi with Vi open in Ti and for all but finitely many i ∈ I holds Vi = Ti. Given I = {a} we have TTa, given I = {a, b} with ab we have TTa ×Tb. Given another family of topological spaces {Si}i∈I such that SiTi for all i ∈ I, we have S = ∏i∈I SiT. If instead Si is a subspace of Ti for each i ∈ I, then S is a subspace of T.

These results are obvious for mathematicians, but formally proven here by means of the Mizar system [3], [2].

Keywords

• topology
• product spaces

• 54B10
• 68T99
• 03B35
Open Access

Binary Representation of Natural Numbers

Published Online: 23 Feb 2019
Page range: 223 - 229

Abstract

Binary representation of integers [5], [3] and arithmetic operations on them have already been introduced in Mizar Mathematical Library [8, 7, 6, 4]. However, these articles formalize the notion of integers as mapped into a certain length tuple of boolean values.

In this article we formalize, by means of Mizar system [2], [1], the binary representation of natural numbers which maps ℕ into bitstreams.

• algorithms

• 68W01
• 68T99
• 03B35
Open Access

Continuity of Bounded Linear Operators on Normed Linear Spaces

Published Online: 23 Feb 2019
Page range: 231 - 237

Abstract

In this article, using the Mizar system [1], [2], we discuss the continuity of bounded linear operators on normed linear spaces. In the first section, it is discussed that bounded linear operators on normed linear spaces are uniformly continuous and Lipschitz continuous. Especially, a bounded linear operator on the dense subset of a complete normed linear space has a unique natural extension over the whole space. In the next section, several basic currying properties are formalized.

In the last section, we formalized that continuity of bilinear operator is equivalent to both Lipschitz continuity and local continuity. We referred to [4], [13], and [3] in this formalization.

Keywords

• Lipschitz continuity
• uniform continuity
• bounded linear operators
• bilinear operators

• 46-00
• 47A07
• 47A30
• 68T99
• 03B35