1. Home
  2. Formalized Mathematics
  3. Volume 26 (2018): Issue 3 (October 2018)

Issues

Journal & Issues

Formalized Mathematics's Cover Image
Formalized Mathematics

Volume 31 (2023): Issue 1 (September 2023)

Volume 30 (2022): Issue 4 (December 2022)

Volume 30 (2022): Issue 3 (October 2022)

Volume 30 (2022): Issue 2 (July 2022)

Volume 30 (2022): Issue 1 (April 2022)

Volume 29 (2021): Issue 4 (December 2021)

Volume 29 (2021): Issue 3 (September 2021)

Volume 29 (2021): Issue 2 (July 2021)

Volume 29 (2021): Issue 1 (April 2021)

Volume 28 (2020): Issue 4 (December 2020)

Volume 28 (2020): Issue 3 (October 2020)

Volume 28 (2020): Issue 2 (July 2020)

Volume 28 (2020): Issue 1 (April 2020)

Volume 27 (2019): Issue 4 (December 2019)

Volume 27 (2019): Issue 3 (October 2019)

Volume 27 (2019): Issue 2 (July 2019)

Volume 27 (2019): Issue 1 (April 2019)

Volume 26 (2018): Issue 4 (December 2018)

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

Volume 26 (2018): Issue 2 (July 2018)

Volume 26 (2018): Issue 1 (April 2018)

Volume 25 (2017): Issue 4 (December 2017)

Volume 25 (2017): Issue 3 (October 2017)

Volume 25 (2017): Issue 2 (July 2017)

Volume 25 (2017): Issue 1 (March 2017)

Volume 24 (2016): Issue 4 (December 2016)

Volume 24 (2016): Issue 3 (September 2016)

Volume 24 (2016): Issue 2 (June 2016)

Volume 24 (2016): Issue 1 (March 2016)

Volume 23 (2015): Issue 4 (December 2015)

Volume 23 (2015): Issue 3 (September 2015)

Volume 23 (2015): Issue 2 (June 2015)

Volume 23 (2015): Issue 1 (March 2015)

Volume 22 (2014): Issue 4 (December 2014)

Volume 22 (2014): Issue 3 (September 2014)

Volume 22 (2014): Issue 2 (June 2014)
Special Issue: 25 years of the Mizar Mathematical Library

Volume 22 (2014): Issue 1 (March 2014)

Volume 21 (2013): Issue 4 (December 2013)

Volume 21 (2013): Issue 3 (October 2013)

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

Volume 21 (2013): Issue 1 (January 2013)

Volume 20 (2012): Issue 4 (December 2012)

Volume 20 (2012): Issue 3 (December 2012)

Volume 20 (2012): Issue 2 (December 2012)

Volume 20 (2012): Issue 1 (January 2012)

Volume 19 (2011): Issue 4 (January 2011)

Volume 19 (2011): Issue 3 (January 2011)

Volume 19 (2011): Issue 2 (January 2011)

Volume 19 (2011): Issue 1 (January 2011)

Volume 18 (2010): Issue 4 (January 2010)

Volume 18 (2010): Issue 3 (January 2010)

Volume 18 (2010): Issue 2 (January 2010)

Volume 18 (2010): Issue 1 (January 2010)

Volume 17 (2009): Issue 4 (January 2009)

Volume 17 (2009): Issue 3 (January 2009)

Volume 17 (2009): Issue 2 (January 2009)

Volume 17 (2009): Issue 1 (January 2009)

Volume 16 (2008): Issue 4 (January 2008)

Volume 16 (2008): Issue 3 (January 2008)

Volume 16 (2008): Issue 2 (January 2008)

Volume 16 (2008): Issue 1 (January 2008)

Volume 15 (2007): Issue 4 (January 2007)

Volume 15 (2007): Issue 3 (January 2007)

Volume 15 (2007): Issue 2 (January 2007)

Volume 15 (2007): Issue 1 (January 2007)

Volume 14 (2006): Issue 4 (January 2006)

Volume 14 (2006): Issue 3 (January 2006)

Volume 14 (2006): Issue 2 (January 2006)

Volume 14 (2006): Issue 1 (January 2006)

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

Search

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

Search

0 Articles
Open Access

Arithmetic Operations on Short Finite Sequences

Rafał Ziobro
Rafał Ziobro
Published Online: 23 Feb 2019
Page range: 199 - 208

Abstract

Summary

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

Some Remarks about Product Spaces

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

Abstract

Summary

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 T ≅ Ta, given I = {a, b} with a≠ b we have T ≅ Ta ×Tb. Given another family of topological spaces {Si}i∈I such that Si ≅ Ti for all i ∈ I, we have S = ∏i∈I Si ≅ T. 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

MSC 2010

  • 54B10
  • 68T99
  • 03B35
Open Access

Binary Representation of Natural Numbers

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

Abstract

Summary

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.

Keywords

  • algorithms

MSC 2010

  • 68W01
  • 68T99
  • 03B35
Open Access

Continuity of Bounded Linear Operators on Normed Linear Spaces

Kazuhisa Nakasho,
Kazuhisa Nakasho,
Yuichi Futa and
Yuichi Futa and
Yasunari Shidama
Yasunari Shidama
Published Online: 23 Feb 2019
Page range: 231 - 237

Abstract

Summary

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

MSC 2010

  • 46-00
  • 47A07
  • 47A30
  • 68T99
  • 03B35
0 Articles
Open Access

Arithmetic Operations on Short Finite Sequences

Rafał Ziobro
Rafał Ziobro
Published Online: 23 Feb 2019
Page range: 199 - 208

Abstract

Summary

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

Some Remarks about Product Spaces

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

Abstract

Summary

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 T ≅ Ta, given I = {a, b} with a≠ b we have T ≅ Ta ×Tb. Given another family of topological spaces {Si}i∈I such that Si ≅ Ti for all i ∈ I, we have S = ∏i∈I Si ≅ T. 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

MSC 2010

  • 54B10
  • 68T99
  • 03B35
Open Access

Binary Representation of Natural Numbers

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

Abstract

Summary

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.

Keywords

  • algorithms

MSC 2010

  • 68W01
  • 68T99
  • 03B35
Open Access

Continuity of Bounded Linear Operators on Normed Linear Spaces

Kazuhisa Nakasho,
Kazuhisa Nakasho,
Yuichi Futa and
Yuichi Futa and
Yasunari Shidama
Yasunari Shidama
Published Online: 23 Feb 2019
Page range: 231 - 237

Abstract

Summary

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

MSC 2010

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