# 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

7 Articles
Accès libre

#### Morley’s Trisector Theorem

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

#### Résumé

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

#### Mots clés

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

• 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é

In this article we introduce necessary notation and definitions to prove the Euler’s Partition Theorem according to H.S. Wilf’s lecture notes . 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/ .

#### Mots clés

• summation method
• flexary plus
• matrix generalization

• 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é

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  (see also ).

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

#### Mots clés

• partition theorem

• 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é

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

#### Mots clés

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

• 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é

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

#### Mots clés

• set partitions
• semiring of sets

• 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

#### Mots clés

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

• 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é

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 .

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” . We take an approach different than that used by Futa et al.  to use in a future article the results obtained by Artur Korniłowicz . 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  using the notion of filters.

#### Mots clés

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

• 20A05
• 20K00
• 03B35

#### MML

• identifier: GROUP_1A
• version: 8.1.045.32.1240