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

#### Search

#### Abstract

The coexistence of “classical”

The paper addresses this problem with another solution, using the Mizar system [3], [2]. Instead of removing one notation it is possible to introduce operators which would concatenate sequences of various types, and in this way allow utilization of the whole range of formalized theorems. While the operation could replace existing FS2XFS, XFS2FS commands (by using empty sequences as initial elements) its universal notation (independent on sequences that are concatenated to the initial object) allows to “forget” about the type of sequences that are concatenated on further positions, and thus simplify the proofs.

#### Keywords

- finite sequence
- finite 0-sequence
- concatenation

#### MSC 2010

- 11B99
- 68T99
- 03B35

Open Access

#### Bilinear Operators on Normed Linear Spaces

Page range: 15 - 23

#### Abstract

The main aim of this article is proving properties of bilinear operators on normed linear spaces formalized by means of Mizar [1]. In the first two chapters, algebraic structures [3] of bilinear operators on linear spaces are discussed. Especially, the space of bounded bilinear operators on normed linear spaces is developed here. In the third chapter, it is remarked that the algebraic structure of bounded bilinear operators to a certain Banach space also constitutes a Banach space.

In the last chapter, the correspondence between the space of bilinear operators and the space of composition of linear opearators is shown. We referred to [4], [11], [2], [7] and [8] in this formalization.

#### Keywords

- Lipschitz continuity
- bounded linear operator
- bilinear operator
- algebraic structure
- Banach space

#### MSC 2010

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

Open Access

#### A Simple Example for Linear Partial Differential Equations and Its Solution Using the Method of Separation of Variables

Page range: 25 - 34

#### Abstract

In this article, we formalized in Mizar [4], [1] simple partial differential equations. In the first section, we formalized partial differentiability and partial derivative. The next section contains the method of separation of variables for one-dimensional wave equation. In the last section, we formalized the superposition principle.We referred to [6], [3], [5] and [9] in this formalization.

#### Keywords

- partial differential equations
- separation of variables
- superposition principle

#### MSC 2010

- 35A08
- 68T99
- 03B35

Open Access

#### Multilinear Operator and Its Basic Properties

Page range: 35 - 45

#### Abstract

In the first chapter, the notion of multilinear operator on real linear spaces is discussed. The algebraic structure [2] of multilinear operators is introduced here. In the second chapter, the results of the first chapter are extended to the case of the normed spaces. This chapter shows that bounded multilinear operators on normed linear spaces constitute the algebraic structure. We referred to [3], [7], [5], [6] in this formalization.

#### Keywords

- Lipschitz continuity
- bounded linear operators
- bilinear operators
- algebraic structure
- Banach space

#### MSC 2010

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

#### Abstract

Using Mizar [1], in the context of a real vector space, we introduce the concept of affine ratio of three aligned points (see [5]).

It is also equivalent to the notion of “Mesure algèbrique”^{1}, to the opposite of the notion of Teilverhältnis^{2} or to the opposite of the ordered length-ratio [9].

In the second part, we introduce the classic notion of “cross-ratio” of 4 points aligned in a real vector space.

Finally, we show that if the real vector space is the real line, the notion corresponds to the classical notion^{3} [9]:

The cross-ratio of a quadruple of distinct points on the real line with coordinates _{1}, _{2}, _{3}, _{4} is given by:

In the Mizar Mathematical Library, the vector spaces were first defined by Kusak, Leonczuk and Muzalewski in the article [6], while the actual real vector space was defined by Trybulec [10] and the complex vector space was defined by Endou [4]. Nakasho and Shidama have developed a solution to explore the notions introduced by different authors^{4} [7]. The definitions can be directly linked in the HTMLized version of the Mizar library^{5}.

The study of the cross-ratio will continue within the framework of the Klein- Beltrami model [2], [3]. For a generalized cross-ratio, see Papadopoulos [8].

#### Keywords

- affine ratio
- cross-ratio
- real vector space
- geometry

#### MSC 2010

- 15A03
- 51A05
- 68T99
- 03B35

Open Access

#### Continuity of Multilinear Operator on Normed Linear Spaces

Page range: 61 - 65

#### Abstract

In this article, various definitions of contuity of multilinear operators on normed linear spaces are discussed in the Mizar formalism [4], [1] and [2]. In the first chapter, several basic theorems are prepared to handle the norm of the multilinear operator, and then it is formalized that the linear space of bounded multilinear operators is a complete Banach space.

In the last chapter, the continuity of the multilinear operator on finite normed spaces is addressed. Especially, it is formalized that the continuity at the origin can be extended to the continuity at every point in its whole domain. We referred to [5], [11], [8], [9] in this formalization.

#### Keywords

- Lipschitz continuity
- bounded linear operators
- multilinear operators
- Banach space

#### MSC 2010

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

#### Abstract

Fubini theorem is an essential tool for the analysis of high-dimensional space [8], [2], [3], a theorem about the multiple integral and iterated integral. The author has been working on formalizing Fubini’s theorem over the past few years [4], [6] in the Mizar system [7], [1]. As a result, Fubini’s theorem (30) was proved in complete form by this article.

#### Keywords

- Fubini’s theorem
- product measure
- multiple integral
- iterated integral

#### MSC 2010

- 28A35
- 68T99
- 03B35

Open Access

#### Tarski Geometry Axioms. Part IV – Right Angle

Page range: 75 - 85

#### Abstract

In the article, we continue [7] the formalization of the work devoted to Tarski’s geometry – the book “Metamathematische Methoden in der Geometrie” (SST for short) by W. Schwabhäuser, W. Szmielew, and A. Tarski [14], [9], [10]. We use the Mizar system to systematically formalize Chapter 8 of the SST book.

We define the notion of right angle and prove some of its basic properties, a theory of intersecting lines (including orthogonality). Using the notion of perpendicular foot, we prove the existence of the midpoint (Satz 8.22), which will be used in the form of the Mizar functor (as the uniqueness can be easily shown) in Chapter 10. In the last section we give some lemmas proven by means of Otter during

#### Keywords

- Tarski geometry
- foundations of geometry
- right angle

#### MSC 2010

- 51A05
- 51M04
- 68T99
- 03B35

Open Access

#### Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm

Page range: 87 - 91

#### Abstract

In this article we formalize in Mizar [1], [2] the maximum number of steps taken by some number theoretical algorithms, “right–to–left binary algorithm” for modular exponentiation and “Euclidean algorithm” [5]. For any natural numbers _{BPow}(^{b}

For “right-to-left binary algorithm”, we formalize the theorem, which says that the required number of the modular squares and modular products in this algorithms are ⌊1+log_{2}_{10} min(

#### Keywords

- algorithms
- power residues
- Euclidean algorithm

#### MSC 2010

- 68W40
- 11A05
- 11A15
- 03B35