Zeszyty czasopisma

Tom 29 (2021): Zeszyt 4 (December 2021)

Tom 29 (2021): Zeszyt 3 (October 2021)

Tom 29 (2021): Zeszyt 2 (July 2021)

Tom 29 (2021): Zeszyt 1 (April 2021)

Tom 28 (2020): Zeszyt 4 (December 2020)

Tom 28 (2020): Zeszyt 3 (October 2020)

Tom 28 (2020): Zeszyt 2 (July 2020)

Tom 28 (2020): Zeszyt 1 (April 2020)

Tom 27 (2019): Zeszyt 4 (December 2019)

Tom 27 (2019): Zeszyt 3 (October 2019)

Tom 27 (2019): Zeszyt 2 (July 2019)

Tom 27 (2019): Zeszyt 1 (April 2019)

Tom 26 (2018): Zeszyt 4 (December 2018)

Tom 26 (2018): Zeszyt 3 (October 2018)

Tom 26 (2018): Zeszyt 2 (July 2018)

Tom 26 (2018): Zeszyt 1 (April 2018)

Tom 25 (2017): Zeszyt 4 (December 2017)

Tom 25 (2017): Zeszyt 3 (October 2017)

Tom 25 (2017): Zeszyt 2 (July 2017)

Tom 25 (2017): Zeszyt 1 (March 2017)

Tom 24 (2016): Zeszyt 4 (December 2016)

Tom 24 (2016): Zeszyt 3 (September 2016)

Tom 24 (2016): Zeszyt 2 (June 2016)

Tom 24 (2016): Zeszyt 1 (March 2016)

Tom 23 (2015): Zeszyt 4 (December 2015)

Tom 23 (2015): Zeszyt 3 (September 2015)

Tom 23 (2015): Zeszyt 2 (June 2015)

Tom 23 (2015): Zeszyt 1 (March 2015)

Tom 22 (2014): Zeszyt 4 (December 2014)

Tom 22 (2014): Zeszyt 3 (September 2014)

Tom 22 (2014): Zeszyt 2 (June 2014)
Special Zeszyt: 25 years of the Mizar Mathematical Library

Tom 22 (2014): Zeszyt 1 (March 2014)

Tom 21 (2013): Zeszyt 4 (December 2013)

Tom 21 (2013): Zeszyt 3 (October 2013)

Tom 21 (2013): Zeszyt 2 (June 2013)

Tom 21 (2013): Zeszyt 1 (January 2013)

Tom 20 (2012): Zeszyt 4 (December 2012)

Tom 20 (2012): Zeszyt 3 (September 2012)

Tom 20 (2012): Zeszyt 2 (June 2012)

Tom 20 (2012): Zeszyt 1 (January 2012)

Tom 19 (2011): Zeszyt 4 (December 2011)

Tom 19 (2011): Zeszyt 3 (September 2011)

Tom 19 (2011): Zeszyt 2 (June 2011)

Tom 19 (2011): Zeszyt 1 (March 2011)

Tom 18 (2010): Zeszyt 4 (December 2010)

Tom 18 (2010): Zeszyt 3 (September 2010)

Tom 18 (2010): Zeszyt 2 (June 2010)

Tom 18 (2010): Zeszyt 1 (March 2010)

Tom 17 (2009): Zeszyt 4 (December 2009)

Tom 17 (2009): Zeszyt 3 (September 2009)

Tom 17 (2009): Zeszyt 2 (June 2009)

Tom 17 (2009): Zeszyt 1 (March 2009)

Tom 16 (2008): Zeszyt 4 (December 2008)

Tom 16 (2008): Zeszyt 3 (September 2008)

Tom 16 (2008): Zeszyt 2 (June 2008)

Tom 16 (2008): Zeszyt 1 (March 2008)

Tom 15 (2007): Zeszyt 4 (December 2007)

Tom 15 (2007): Zeszyt 3 (September 2007)

Tom 15 (2007): Zeszyt 2 (June 2007)

Tom 15 (2007): Zeszyt 1 (March 2007)

Tom 14 (2006): Zeszyt 4 (December 2006)

Tom 14 (2006): Zeszyt 3 (September 2006)

Tom 14 (2006): Zeszyt 2 (June 2006)

Tom 14 (2006): Zeszyt 1 (March 2006)

Informacje o czasopiśmie
Format
Czasopismo
eISSN
1898-9934
Pierwsze wydanie
09 Jun 2008
Częstotliwość wydawania
4 razy w roku
Języki
Angielski

Wyszukiwanie

Tom 24 (2016): Zeszyt 3 (September 2016)

Informacje o czasopiśmie
Format
Czasopismo
eISSN
1898-9934
Pierwsze wydanie
09 Jun 2008
Częstotliwość wydawania
4 razy w roku
Języki
Angielski

Wyszukiwanie

7 Artykułów
Otwarty dostęp

Compactness in Metric Spaces

Data publikacji: 21 Feb 2017
Zakres stron: 167 - 172

Abstrakt

Słowa kluczowe

  • metric spaces
  • normed linear spaces
  • compactness

MSC

  • 46B50
  • 54E45
  • 03B35

MML

  • identifier: TOPMETR4
  • version: 8.1.05 5.37.1275
Otwarty dostęp

Double Sequences and Iterated Limits in Regular Space

Data publikacji: 21 Feb 2017
Zakres stron: 173 - 186

Abstrakt

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].

Słowa kluczowe

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

MSC

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

MML

  • identifier: CARDFIL4
  • version: 8.1.05 5.37.1275
Otwarty dostęp

Prime Factorization of Sums and Differences of Two Like Powers

Data publikacji: 21 Feb 2017
Zakres stron: 187 - 198

Abstrakt

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].

Słowa kluczowe

  • integers
  • factorization
  • primes

MSC

  • 11A51
  • 03B35

MML

  • identifier: NEWTON03
  • version: 8.1.05 5.37.1275
Otwarty dostęp

Riemann-Stieltjes Integral

Data publikacji: 21 Feb 2017
Zakres stron: 199 - 204

Abstrakt

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].

Słowa kluczowe

  • Riemann-Stieltjes integral
  • bounded variation
  • linearity

MSC

  • 26A42
  • 26A45
  • 03B35

MML

  • identifier: INTEGR22
  • version: 8.1.05 5.37.1275
Otwarty dostęp

Quasi-uniform Space

Data publikacji: 21 Feb 2017
Zakres stron: 205 - 214

Abstrakt

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.

Słowa kluczowe

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

MSC

  • 54E15
  • 03B35

MML

  • identifier: UNIFORM2
  • version: 8.1.05 5.37.1275
Otwarty dostęp

Uniform Space

Data publikacji: 21 Feb 2017
Zakres stron: 215 - 226

Abstrakt

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.

Słowa kluczowe

  • 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
Otwarty dostęp

Some Algebraic Properties of Polynomial Rings

Data publikacji: 21 Feb 2017
Zakres stron: 227 - 237

Abstrakt

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.

Słowa kluczowe

  • polynomial
  • polynomial ring
  • polynomial GCD

MSC

  • 12E05
  • 11T55
  • 03B35

MML

  • identifier: RING_4
  • version: 8.1.05 5.37.1275
7 Artykułów
Otwarty dostęp

Compactness in Metric Spaces

Data publikacji: 21 Feb 2017
Zakres stron: 167 - 172

Abstrakt

Słowa kluczowe

  • metric spaces
  • normed linear spaces
  • compactness

MSC

  • 46B50
  • 54E45
  • 03B35

MML

  • identifier: TOPMETR4
  • version: 8.1.05 5.37.1275
Otwarty dostęp

Double Sequences and Iterated Limits in Regular Space

Data publikacji: 21 Feb 2017
Zakres stron: 173 - 186

Abstrakt

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].

Słowa kluczowe

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

MSC

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

MML

  • identifier: CARDFIL4
  • version: 8.1.05 5.37.1275
Otwarty dostęp

Prime Factorization of Sums and Differences of Two Like Powers

Data publikacji: 21 Feb 2017
Zakres stron: 187 - 198

Abstrakt

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].

Słowa kluczowe

  • integers
  • factorization
  • primes

MSC

  • 11A51
  • 03B35

MML

  • identifier: NEWTON03
  • version: 8.1.05 5.37.1275
Otwarty dostęp

Riemann-Stieltjes Integral

Data publikacji: 21 Feb 2017
Zakres stron: 199 - 204

Abstrakt

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].

Słowa kluczowe

  • Riemann-Stieltjes integral
  • bounded variation
  • linearity

MSC

  • 26A42
  • 26A45
  • 03B35

MML

  • identifier: INTEGR22
  • version: 8.1.05 5.37.1275
Otwarty dostęp

Quasi-uniform Space

Data publikacji: 21 Feb 2017
Zakres stron: 205 - 214

Abstrakt

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.

Słowa kluczowe

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

MSC

  • 54E15
  • 03B35

MML

  • identifier: UNIFORM2
  • version: 8.1.05 5.37.1275
Otwarty dostęp

Uniform Space

Data publikacji: 21 Feb 2017
Zakres stron: 215 - 226

Abstrakt

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.

Słowa kluczowe

  • 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
Otwarty dostęp

Some Algebraic Properties of Polynomial Rings

Data publikacji: 21 Feb 2017
Zakres stron: 227 - 237

Abstrakt

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.

Słowa kluczowe

  • polynomial
  • polynomial ring
  • polynomial GCD

MSC

  • 12E05
  • 11T55
  • 03B35

MML

  • identifier: RING_4
  • version: 8.1.05 5.37.1275

Zaplanuj zdalną konferencję ze Sciendo