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

#### Search

Open Access

#### Derivation of Commutative Rings and the Leibniz Formula for Power of Derivation

Page range: 1 - 8

#### Abstract

In this article we formalize in Mizar [1], [2] a derivation of commutative rings, its definition and some properties. The details are to be referred to [5], [7]. A derivation of a ring, say

A derivation is a map

(i)

(ii)

Typical properties are formalized such as:

We also formalized the Leibniz Formula for power of derivation

Lastly applying the definition to the polynomial ring of

#### Keywords

- derivation
- Leibniz Formula
- derivation of polynomial ring

#### MSC

- 13B25
- 13N15
- 68V20

#### Abstract

In this article we formalize in Mizar [1], [2] the inverse function theorem for the class of ^{1} functions between Banach spaces. In the first section, we prove several theorems about open sets in real norm space, which are needed in the proof of the inverse function theorem. In the next section, we define a function to exchange the order of a product of two normed spaces, namely 𝔼 ↶ ≂ (

In the third section, using the implicit function theorem, we prove a theorem that is a necessary component of the proof of the inverse function theorem. In the last section, we finally formalized an inverse function theorem for class of ^{1} functions between Banach spaces. We referred to [9], [10], and [3] in the formalization.

#### Keywords

- inverse function theorem
- Lipschitz continuity
- differentiability
- implicit function
- inverse function

#### MSC

- 26B10
- 47A05
- 47J07
- 68V20

Open Access

#### Miscellaneous Graph Preliminaries. Part I

Page range: 21 - 38

#### Abstract

This article contains many auxiliary theorems which were missing in the Mizar Mathematical Library to the best of the author’s knowledge. Most of them regard graph theory as formalized in the GLIB series and are needed in upcoming articles.

#### Keywords

- graph

#### MSC

- 05C99
- 68V20

#### Abstract

In this article we further develop field theory in Mizar [1], [2], [3] towards splitting fields. We deal with algebraic extensions [4], [5]: a field extension

#### Keywords

- algebraic extensions
- finite extensions
- field of algebraic numbers

#### MSC

- 12F05
- 68V20

Open Access

#### Functional Space Consisted by Continuous Functions on Topological Space

Page range: 49 - 62

#### Abstract

In this article, using the Mizar system [1], [2], first we give a definition of a functional space which is constructed from all continuous functions defined on a compact topological space [5]. We prove that this functional space is a Banach space [3]. Next, we give a definition of a function space which is constructed from all continuous functions with bounded support. We also prove that this function space is a normed space.

#### Keywords

- continuous function space
- compact topological space
- Banach space

#### MSC

- 46E10
- 68V20

Open Access

#### Elementary Number Theory Problems. Part II

Page range: 63 - 68

#### Abstract

In this paper problems 14, 15, 29, 30, 34, 78, 83, 97, and 116 from [6] are formalized, using the Mizar formalism [1], [2], [3]. Some properties related to the divisibility of prime numbers were proved. It has been shown that the equation of the form ^{2} + 1 = ^{2} + ^{2}, where ^{2}^{n}

#### Keywords

- number theory
- divisibility
- primes

#### MSC

- 11A41
- 03B35
- 68V20