Magazine et Edition

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

Volume 29 (2021): Edition 3 (October 2021)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Volume 20 (2012): Edition 3 (September 2012)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Détails du magazine
Format
Magazine
eISSN
1898-9934
Première publication
09 Jun 2008
Période de publication
4 fois par an
Langues
Anglais

Chercher

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

Détails du magazine
Format
Magazine
eISSN
1898-9934
Première publication
09 Jun 2008
Période de publication
4 fois par an
Langues
Anglais

Chercher

7 Articles
Accès libre

Morley’s Trisector Theorem

Publié en ligne: 13 Aug 2015
Pages: 75 - 79

Résumé

Abstract

Morley’s trisector theorem states that “The points of intersection of the adjacent trisectors of the angles of any triangle are the vertices of an equilateral triangle” [10]. There are many proofs of Morley’s trisector theorem [12, 16, 9, 13, 8, 20, 3, 18]. We follow the proof given by A. Letac in [15].

Mots clés

  • Euclidean geometry
  • Morley’s trisector theorem
  • equilateral triangle

MSC

  • 51M04
  • 03B35

MML

  • identifier: EUCLID11
  • version: 8.1.045.32.1237
Accès libre

Flexary Operations

Publié en ligne: 13 Aug 2015
Pages: 81 - 92

Résumé

Abstract

In this article we introduce necessary notation and definitions to prove the Euler’s Partition Theorem according to H.S. Wilf’s lecture notes [31]. Our aim is to create an environment which allows to formalize the theorem in a way that is as similar as possible to the original informal proof.

Euler’s Partition Theorem is listed as item #45 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/ [30].

Mots clés

  • summation method
  • flexary plus
  • matrix generalization

MSC

  • 11B99
  • 03B35

MML

  • identifier: FLEXARY1
  • version: 8.1.045.32.1237
Accès libre

Euler’s Partition Theorem

Publié en ligne: 13 Aug 2015
Pages: 93 - 99

Résumé

Abstract

In this article we prove the Euler’s Partition Theorem which states that the number of integer partitions with odd parts equals the number of partitions with distinct parts. The formalization follows H.S. Wilf’s lecture notes [28] (see also [1]).

Euler’s Partition Theorem is listed as item #45 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/ [27].

Mots clés

  • partition theorem

MSC

  • 05A17
  • 03B35

MML

  • identifier: EULRPART
  • version: 8.1.045.32.1237
Accès libre

Introduction to Diophantine Approximation

Publié en ligne: 13 Aug 2015
Pages: 101 - 106

Résumé

Abstract

In this article we formalize some results of Diophantine approximation, i.e. the approximation of an irrational number by rationals. A typical example is finding an integer solution (x, y) of the inequality |xθ − y| ≤ 1/x, where 0 is a real number. First, we formalize some lemmas about continued fractions. Then we prove that the inequality has infinitely many solutions by continued fractions. Finally, we formalize Dirichlet’s proof (1842) of existence of the solution [12], [1].

Mots clés

  • irrational number
  • approximation
  • continued fraction
  • rational number
  • Dirichlet’s proof

MSC

  • 11A55
  • 11J68
  • 03B35

MML

  • identifier: DIOPHAN1
  • version: 8.1.045.32.1237
Accès libre

Finite Product of Semiring of Sets

Publié en ligne: 13 Aug 2015
Pages: 107 - 114

Résumé

Abstract

We formalize that the image of a semiring of sets [17] by an injective function is a semiring of sets.We offer a non-trivial example of a semiring of sets in a topological space [21]. Finally, we show that the finite product of a semiring of sets is also a semiring of sets [21] and that the finite product of a classical semiring of sets [8] is a classical semiring of sets. In this case, we use here the notation from the book of Aliprantis and Border [1].

Mots clés

  • set partitions
  • semiring of sets

MSC

  • 28A05
  • 03E02
  • 03B35

MML

  • identifier: SRINGS_4
  • version: 8.1.045.32.1237
Accès libre

Two Axiomatizations of Nelson Algebras

Publié en ligne: 13 Aug 2015
Pages: 115 - 125

Résumé

Mots clés

  • quasi-pseudo-Boolean algebras
  • Nelson lattices
  • de Morgan lattices

MSC

  • 06D30
  • 08A05
  • 03B35

MML

  • identifier: NELSON_1
  • version: 8.1.045.32.1237
Accès libre

Groups – Additive Notation

Publié en ligne: 13 Aug 2015
Pages: 127 - 160

Résumé

Abstract

We translate the articles covering group theory already available in the Mizar Mathematical Library from multiplicative into additive notation. We adapt the works of Wojciech A. Trybulec [41, 42, 43] and Artur Korniłowicz [25].

In particular, these authors have defined the notions of group, abelian group, power of an element of a group, order of a group and order of an element, subgroup, coset of a subgroup, index of a subgroup, conjugation, normal subgroup, topological group, dense subset and basis of a topological group. Lagrange’s theorem and some other theorems concerning these notions [9, 24, 22] are presented.

Note that “The term ℤ-module is simply another name for an additive abelian group” [27]. We take an approach different than that used by Futa et al. [21] to use in a future article the results obtained by Artur Korniłowicz [25]. Indeed, Hölzl et al. showed that it was possible to build “a generic theory of limits based on filters” in Isabelle/HOL [23, 10]. Our goal is to define the convergence of a sequence and the convergence of a series in an abelian topological group [11] using the notion of filters.

Mots clés

  • additive group
  • subgroup
  • Lagrange theorem
  • conjugation
  • normal subgroup
  • index
  • additive topological group
  • basis
  • neighborhood
  • additive abelian group
  • Z-module

MSC

  • 20A05
  • 20K00
  • 03B35

MML

  • identifier: GROUP_1A
  • version: 8.1.045.32.1240
7 Articles
Accès libre

Morley’s Trisector Theorem

Publié en ligne: 13 Aug 2015
Pages: 75 - 79

Résumé

Abstract

Morley’s trisector theorem states that “The points of intersection of the adjacent trisectors of the angles of any triangle are the vertices of an equilateral triangle” [10]. There are many proofs of Morley’s trisector theorem [12, 16, 9, 13, 8, 20, 3, 18]. We follow the proof given by A. Letac in [15].

Mots clés

  • Euclidean geometry
  • Morley’s trisector theorem
  • equilateral triangle

MSC

  • 51M04
  • 03B35

MML

  • identifier: EUCLID11
  • version: 8.1.045.32.1237
Accès libre

Flexary Operations

Publié en ligne: 13 Aug 2015
Pages: 81 - 92

Résumé

Abstract

In this article we introduce necessary notation and definitions to prove the Euler’s Partition Theorem according to H.S. Wilf’s lecture notes [31]. Our aim is to create an environment which allows to formalize the theorem in a way that is as similar as possible to the original informal proof.

Euler’s Partition Theorem is listed as item #45 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/ [30].

Mots clés

  • summation method
  • flexary plus
  • matrix generalization

MSC

  • 11B99
  • 03B35

MML

  • identifier: FLEXARY1
  • version: 8.1.045.32.1237
Accès libre

Euler’s Partition Theorem

Publié en ligne: 13 Aug 2015
Pages: 93 - 99

Résumé

Abstract

In this article we prove the Euler’s Partition Theorem which states that the number of integer partitions with odd parts equals the number of partitions with distinct parts. The formalization follows H.S. Wilf’s lecture notes [28] (see also [1]).

Euler’s Partition Theorem is listed as item #45 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/ [27].

Mots clés

  • partition theorem

MSC

  • 05A17
  • 03B35

MML

  • identifier: EULRPART
  • version: 8.1.045.32.1237
Accès libre

Introduction to Diophantine Approximation

Publié en ligne: 13 Aug 2015
Pages: 101 - 106

Résumé

Abstract

In this article we formalize some results of Diophantine approximation, i.e. the approximation of an irrational number by rationals. A typical example is finding an integer solution (x, y) of the inequality |xθ − y| ≤ 1/x, where 0 is a real number. First, we formalize some lemmas about continued fractions. Then we prove that the inequality has infinitely many solutions by continued fractions. Finally, we formalize Dirichlet’s proof (1842) of existence of the solution [12], [1].

Mots clés

  • irrational number
  • approximation
  • continued fraction
  • rational number
  • Dirichlet’s proof

MSC

  • 11A55
  • 11J68
  • 03B35

MML

  • identifier: DIOPHAN1
  • version: 8.1.045.32.1237
Accès libre

Finite Product of Semiring of Sets

Publié en ligne: 13 Aug 2015
Pages: 107 - 114

Résumé

Abstract

We formalize that the image of a semiring of sets [17] by an injective function is a semiring of sets.We offer a non-trivial example of a semiring of sets in a topological space [21]. Finally, we show that the finite product of a semiring of sets is also a semiring of sets [21] and that the finite product of a classical semiring of sets [8] is a classical semiring of sets. In this case, we use here the notation from the book of Aliprantis and Border [1].

Mots clés

  • set partitions
  • semiring of sets

MSC

  • 28A05
  • 03E02
  • 03B35

MML

  • identifier: SRINGS_4
  • version: 8.1.045.32.1237
Accès libre

Two Axiomatizations of Nelson Algebras

Publié en ligne: 13 Aug 2015
Pages: 115 - 125

Résumé

Mots clés

  • quasi-pseudo-Boolean algebras
  • Nelson lattices
  • de Morgan lattices

MSC

  • 06D30
  • 08A05
  • 03B35

MML

  • identifier: NELSON_1
  • version: 8.1.045.32.1237
Accès libre

Groups – Additive Notation

Publié en ligne: 13 Aug 2015
Pages: 127 - 160

Résumé

Abstract

We translate the articles covering group theory already available in the Mizar Mathematical Library from multiplicative into additive notation. We adapt the works of Wojciech A. Trybulec [41, 42, 43] and Artur Korniłowicz [25].

In particular, these authors have defined the notions of group, abelian group, power of an element of a group, order of a group and order of an element, subgroup, coset of a subgroup, index of a subgroup, conjugation, normal subgroup, topological group, dense subset and basis of a topological group. Lagrange’s theorem and some other theorems concerning these notions [9, 24, 22] are presented.

Note that “The term ℤ-module is simply another name for an additive abelian group” [27]. We take an approach different than that used by Futa et al. [21] to use in a future article the results obtained by Artur Korniłowicz [25]. Indeed, Hölzl et al. showed that it was possible to build “a generic theory of limits based on filters” in Isabelle/HOL [23, 10]. Our goal is to define the convergence of a sequence and the convergence of a series in an abelian topological group [11] using the notion of filters.

Mots clés

  • additive group
  • subgroup
  • Lagrange theorem
  • conjugation
  • normal subgroup
  • index
  • additive topological group
  • basis
  • neighborhood
  • additive abelian group
  • Z-module

MSC

  • 20A05
  • 20K00
  • 03B35

MML

  • identifier: GROUP_1A
  • version: 8.1.045.32.1240

Planifiez votre conférence à distance avec Sciendo