Issues

Journal & Issues

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

Volume 29 (2021): Issue 3 (October 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 (September 2012)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Search

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

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

Search

7 Articles
access type Open Access

Compactness in Metric Spaces

Published Online: 21 Feb 2017
Page range: 167 - 172

Abstract

Summary

In this article, we mainly formalize in Mizar [2] the equivalence among a few compactness definitions of metric spaces, norm spaces, and the real line. In the first section, we formalized general topological properties of metric spaces. We discussed openness and closedness of subsets in metric spaces in terms of convergence of element sequences. In the second section, we firstly formalize the definition of sequentially compact, and then discuss the equivalence of compactness, countable compactness, sequential compactness, and totally boundedness with completeness in metric spaces.

In the third section, we discuss compactness in norm spaces. We formalize the equivalence of compactness and sequential compactness in norm space. In the fourth section, we formalize topological properties of the real line in terms of convergence of real number sequences. In the last section, we formalize the equivalence of compactness and sequential compactness in the real line. These formalizations are based on [20], [5], [17], [14], and [4].

Keywords

  • metric spaces
  • normed linear spaces
  • compactness

MSC

  • 46B50
  • 54E45
  • 03B35

MML

  • identifier: TOPMETR4
  • version: 8.1.05 5.37.1275
access type Open Access

Double Sequences and Iterated Limits in Regular Space

Published Online: 21 Feb 2017
Page range: 173 - 186

Abstract

Abstract

First, we define in Mizar [5], the Cartesian product of two filters bases and the Cartesian product of two filters. After comparing the product of two Fréchet filters on ℕ (F1) with the Fréchet filter on ℕ × ℕ (F2), we compare limF₁ and limF₂ for all double sequences in a non empty topological space.

Endou, Okazaki and Shidama formalized in [14] the “convergence in Pringsheim’s sense” for double sequence of real numbers. We show some basic correspondences between the p-convergence and the filter convergence in a topological space. Then we formalize that the double sequence converges in “Pringsheim’s sense” but not in Frechet filter on ℕ × ℕ sense.

In the next section, we generalize some definitions: “is convergent in the first coordinate”, “is convergent in the second coordinate”, “the lim in the first coordinate of”, “the lim in the second coordinate of” according to [14], in Hausdorff space.

Finally, we generalize two theorems: (3) and (4) from [14] in the case of double sequences and we formalize the “iterated limit” theorem (“Double limit” [7], p. 81, par. 8.5 “Double limite” [6] (TG I,57)), all in regular space. We were inspired by the exercises (2.11.4), (2.17.5) [17] and the corrections B.10 [18].

Keywords

  • filter
  • double limits
  • Pringsheim convergence
  • iterated limits
  • regular space

MSC

  • 54A20
  • 40A05
  • 40B05
  • 03B35

MML

  • identifier: CARDFIL4
  • version: 8.1.05 5.37.1275
access type Open Access

Prime Factorization of Sums and Differences of Two Like Powers

Published Online: 21 Feb 2017
Page range: 187 - 198

Abstract

Abstract

Representation of a non zero integer as a signed product of primes is unique similarly to its representations in various types of positional notations [4], [3]. The study focuses on counting the prime factors of integers in the form of sums or differences of two equal powers (thus being represented by 1 and a series of zeroes in respective digital bases).

Although the introduced theorems are not particularly important, they provide a couple of shortcuts useful for integer factorization, which could serve in further development of Mizar projects [2]. This could be regarded as one of the important benefits of proof formalization [9].

Keywords

  • integers
  • factorization
  • primes

MSC

  • 11A51
  • 03B35

MML

  • identifier: NEWTON03
  • version: 8.1.05 5.37.1275
access type Open Access

Riemann-Stieltjes Integral

Published Online: 21 Feb 2017
Page range: 199 - 204

Abstract

Abstract

In this article, the definitions and basic properties of Riemann-Stieltjes integral are formalized in Mizar [1]. In the first section, we showed the preliminary definition. We proved also some properties of finite sequences of real numbers. In Sec. 2, we defined variation. Using the definition, we also defined bounded variation and total variation, and proved theorems about related properties.

In Sec. 3, we defined Riemann-Stieltjes integral. Referring to the way of the article [7], we described the definitions. In the last section, we proved theorems about linearity of Riemann-Stieltjes integral. Because there are two types of linearity in Riemann-Stieltjes integral, we proved linearity in two ways. We showed the proof of theorems based on the description of the article [7]. These formalizations are based on [8], [5], [3], and [4].

Keywords

  • Riemann-Stieltjes integral
  • bounded variation
  • linearity

MSC

  • 26A42
  • 26A45
  • 03B35

MML

  • identifier: INTEGR22
  • version: 8.1.05 5.37.1275
access type Open Access

Quasi-uniform Space

Published Online: 21 Feb 2017
Page range: 205 - 214

Abstract

Abstract

In this article, using mostly Pervin [9], Kunzi [6], [8], [7], Williams [11] and Bourbaki [3] works, we formalize in Mizar [2] the notions of quasiuniform space, semi-uniform space and locally uniform space.

We define the topology induced by a quasi-uniform space. Finally we formalize from the sets of the form ((X \ Ω) × X) ∪ (X × Ω), the Csaszar-Pervin quasi-uniform space induced by a topological space.

Keywords

  • quasi-uniform space
  • quasi-uniformity
  • Pervin space
  • Csaszar-Pervin quasi-uniformity

MSC

  • 54E15
  • 03B35

MML

  • identifier: UNIFORM2
  • version: 8.1.05 5.37.1275
access type Open Access

Uniform Space

Published Online: 21 Feb 2017
Page range: 215 - 226

Abstract

Abstract

In this article, we formalize in Mizar [1] the notion of uniform space introduced by André Weil using the concepts of entourages [2].

We present some results between uniform space and pseudo metric space. We introduce the concepts of left-uniformity and right-uniformity of a topological group.

Next, we define the concept of the partition topology. Following the Vlach’s works [11, 10], we define the semi-uniform space induced by a tolerance and the uniform space induced by an equivalence relation.

Finally, using mostly Gehrke, Grigorieff and Pin [4] works, a Pervin uniform space defined from the sets of the form ((X\A) × (X\A)) ∪ (A×A) is presented.

Keywords

  • uniform space
  • uniformity
  • pseudo-metric space
  • topological group
  • partition topology
  • Pervin uniform space

MSC

  • 54E15
  • 03B35

MML

  • identifier: UNIFORM3
  • version: 8.1.05 5.37.1275
access type Open Access

Some Algebraic Properties of Polynomial Rings

Published Online: 21 Feb 2017
Page range: 227 - 237

Abstract

Abstract

In this article we extend the algebraic theory of polynomial rings, formalized in Mizar [1], based on [2], [3]. After introducing constant and monic polynomials we present the canonical embedding of R into R[X] and deal with both unit and irreducible elements. We also define polynomial GCDs and show that for fields F and irreducible polynomials p the field F[X]/<p> is isomorphic to the field of polynomials with degree smaller than the one of p.

Keywords

  • polynomial
  • polynomial ring
  • polynomial GCD

MSC

  • 12E05
  • 11T55
  • 03B35

MML

  • identifier: RING_4
  • version: 8.1.05 5.37.1275
7 Articles
access type Open Access

Compactness in Metric Spaces

Published Online: 21 Feb 2017
Page range: 167 - 172

Abstract

Summary

In this article, we mainly formalize in Mizar [2] the equivalence among a few compactness definitions of metric spaces, norm spaces, and the real line. In the first section, we formalized general topological properties of metric spaces. We discussed openness and closedness of subsets in metric spaces in terms of convergence of element sequences. In the second section, we firstly formalize the definition of sequentially compact, and then discuss the equivalence of compactness, countable compactness, sequential compactness, and totally boundedness with completeness in metric spaces.

In the third section, we discuss compactness in norm spaces. We formalize the equivalence of compactness and sequential compactness in norm space. In the fourth section, we formalize topological properties of the real line in terms of convergence of real number sequences. In the last section, we formalize the equivalence of compactness and sequential compactness in the real line. These formalizations are based on [20], [5], [17], [14], and [4].

Keywords

  • metric spaces
  • normed linear spaces
  • compactness

MSC

  • 46B50
  • 54E45
  • 03B35

MML

  • identifier: TOPMETR4
  • version: 8.1.05 5.37.1275
access type Open Access

Double Sequences and Iterated Limits in Regular Space

Published Online: 21 Feb 2017
Page range: 173 - 186

Abstract

Abstract

First, we define in Mizar [5], the Cartesian product of two filters bases and the Cartesian product of two filters. After comparing the product of two Fréchet filters on ℕ (F1) with the Fréchet filter on ℕ × ℕ (F2), we compare limF₁ and limF₂ for all double sequences in a non empty topological space.

Endou, Okazaki and Shidama formalized in [14] the “convergence in Pringsheim’s sense” for double sequence of real numbers. We show some basic correspondences between the p-convergence and the filter convergence in a topological space. Then we formalize that the double sequence converges in “Pringsheim’s sense” but not in Frechet filter on ℕ × ℕ sense.

In the next section, we generalize some definitions: “is convergent in the first coordinate”, “is convergent in the second coordinate”, “the lim in the first coordinate of”, “the lim in the second coordinate of” according to [14], in Hausdorff space.

Finally, we generalize two theorems: (3) and (4) from [14] in the case of double sequences and we formalize the “iterated limit” theorem (“Double limit” [7], p. 81, par. 8.5 “Double limite” [6] (TG I,57)), all in regular space. We were inspired by the exercises (2.11.4), (2.17.5) [17] and the corrections B.10 [18].

Keywords

  • filter
  • double limits
  • Pringsheim convergence
  • iterated limits
  • regular space

MSC

  • 54A20
  • 40A05
  • 40B05
  • 03B35

MML

  • identifier: CARDFIL4
  • version: 8.1.05 5.37.1275
access type Open Access

Prime Factorization of Sums and Differences of Two Like Powers

Published Online: 21 Feb 2017
Page range: 187 - 198

Abstract

Abstract

Representation of a non zero integer as a signed product of primes is unique similarly to its representations in various types of positional notations [4], [3]. The study focuses on counting the prime factors of integers in the form of sums or differences of two equal powers (thus being represented by 1 and a series of zeroes in respective digital bases).

Although the introduced theorems are not particularly important, they provide a couple of shortcuts useful for integer factorization, which could serve in further development of Mizar projects [2]. This could be regarded as one of the important benefits of proof formalization [9].

Keywords

  • integers
  • factorization
  • primes

MSC

  • 11A51
  • 03B35

MML

  • identifier: NEWTON03
  • version: 8.1.05 5.37.1275
access type Open Access

Riemann-Stieltjes Integral

Published Online: 21 Feb 2017
Page range: 199 - 204

Abstract

Abstract

In this article, the definitions and basic properties of Riemann-Stieltjes integral are formalized in Mizar [1]. In the first section, we showed the preliminary definition. We proved also some properties of finite sequences of real numbers. In Sec. 2, we defined variation. Using the definition, we also defined bounded variation and total variation, and proved theorems about related properties.

In Sec. 3, we defined Riemann-Stieltjes integral. Referring to the way of the article [7], we described the definitions. In the last section, we proved theorems about linearity of Riemann-Stieltjes integral. Because there are two types of linearity in Riemann-Stieltjes integral, we proved linearity in two ways. We showed the proof of theorems based on the description of the article [7]. These formalizations are based on [8], [5], [3], and [4].

Keywords

  • Riemann-Stieltjes integral
  • bounded variation
  • linearity

MSC

  • 26A42
  • 26A45
  • 03B35

MML

  • identifier: INTEGR22
  • version: 8.1.05 5.37.1275
access type Open Access

Quasi-uniform Space

Published Online: 21 Feb 2017
Page range: 205 - 214

Abstract

Abstract

In this article, using mostly Pervin [9], Kunzi [6], [8], [7], Williams [11] and Bourbaki [3] works, we formalize in Mizar [2] the notions of quasiuniform space, semi-uniform space and locally uniform space.

We define the topology induced by a quasi-uniform space. Finally we formalize from the sets of the form ((X \ Ω) × X) ∪ (X × Ω), the Csaszar-Pervin quasi-uniform space induced by a topological space.

Keywords

  • quasi-uniform space
  • quasi-uniformity
  • Pervin space
  • Csaszar-Pervin quasi-uniformity

MSC

  • 54E15
  • 03B35

MML

  • identifier: UNIFORM2
  • version: 8.1.05 5.37.1275
access type Open Access

Uniform Space

Published Online: 21 Feb 2017
Page range: 215 - 226

Abstract

Abstract

In this article, we formalize in Mizar [1] the notion of uniform space introduced by André Weil using the concepts of entourages [2].

We present some results between uniform space and pseudo metric space. We introduce the concepts of left-uniformity and right-uniformity of a topological group.

Next, we define the concept of the partition topology. Following the Vlach’s works [11, 10], we define the semi-uniform space induced by a tolerance and the uniform space induced by an equivalence relation.

Finally, using mostly Gehrke, Grigorieff and Pin [4] works, a Pervin uniform space defined from the sets of the form ((X\A) × (X\A)) ∪ (A×A) is presented.

Keywords

  • uniform space
  • uniformity
  • pseudo-metric space
  • topological group
  • partition topology
  • Pervin uniform space

MSC

  • 54E15
  • 03B35

MML

  • identifier: UNIFORM3
  • version: 8.1.05 5.37.1275
access type Open Access

Some Algebraic Properties of Polynomial Rings

Published Online: 21 Feb 2017
Page range: 227 - 237

Abstract

Abstract

In this article we extend the algebraic theory of polynomial rings, formalized in Mizar [1], based on [2], [3]. After introducing constant and monic polynomials we present the canonical embedding of R into R[X] and deal with both unit and irreducible elements. We also define polynomial GCDs and show that for fields F and irreducible polynomials p the field F[X]/<p> is isomorphic to the field of polynomials with degree smaller than the one of p.

Keywords

  • polynomial
  • polynomial ring
  • polynomial GCD

MSC

  • 12E05
  • 11T55
  • 03B35

MML

  • identifier: RING_4
  • version: 8.1.05 5.37.1275

Plan your remote conference with Sciendo