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

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

0 Articles
Open Access

#### Morley’s Trisector Theorem

Published Online: 13 Aug 2015
Page range: 75 - 79

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

#### Keywords

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

• 51M04
• 03B35

#### MML

• identifier: EUCLID11
• version: 8.1.045.32.1237
Open Access

#### Flexary Operations

Published Online: 13 Aug 2015
Page range: 81 - 92

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

#### Keywords

• summation method
• flexary plus
• matrix generalization

• 11B99
• 03B35

#### MML

• identifier: FLEXARY1
• version: 8.1.045.32.1237
Open Access

#### Euler’s Partition Theorem

Published Online: 13 Aug 2015
Page range: 93 - 99

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

#### Keywords

• partition theorem

• 05A17
• 03B35

#### MML

• identifier: EULRPART
• version: 8.1.045.32.1237
Open Access

#### Introduction to Diophantine Approximation

Published Online: 13 Aug 2015
Page range: 101 - 106

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

#### Keywords

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

• 11A55
• 11J68
• 03B35

#### MML

• identifier: DIOPHAN1
• version: 8.1.045.32.1237
Open Access

#### Finite Product of Semiring of Sets

Published Online: 13 Aug 2015
Page range: 107 - 114

#### Abstract

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 .

#### Keywords

• set partitions
• semiring of sets

• 28A05
• 03E02
• 03B35

#### MML

• identifier: SRINGS_4
• version: 8.1.045.32.1237
Open Access

#### Two Axiomatizations of Nelson Algebras

Published Online: 13 Aug 2015
Page range: 115 - 125

#### Abstract

Nelson algebras were first studied by Rasiowa and Białynicki- Birula  under the name N-lattices or quasi-pseudo-Boolean algebras. Later, in investigations by Monteiro and Brignole [3, 4], and  the name “Nelson algebras” was adopted - which is now commonly used to show the correspondence with Nelson’s paper  on constructive logic with strong negation.

By a Nelson algebra we mean an abstract algebra

〈L, T, -, ¬, →, ⇒, ⊔, ⊓〉

where L is the carrier, − is a quasi-complementation (Rasiowa used the sign ~, but in Mizar “−” should be used to follow the approach described in  and ), ¬ is a weak pseudo-complementation → is weak relative pseudocomplementation and ⇒ is implicative operation. ⊔ and ⊓ are ordinary lattice binary operations of supremum and infimum.

In this article we give the definition and basic properties of these algebras according to  and . We start with preliminary section on quasi-Boolean algebras (i.e. de Morgan bounded lattices). Later we give the axioms in the form of Mizar adjectives with names corresponding with those in . As our main result we give two axiomatizations (non-equational and equational) and the full formal proof of their equivalence.

The second set of equations is rather long but it shows the logical essence of Nelson lattices. This formalization aims at the construction of algebraic model of rough sets  in our future submissions. Section 4 contains all items from Th. 1.2 and 1.3 (and the itemization is given in the text). In the fifth section we provide full formal proof of Th. 2.1 p. 75 .

#### Keywords

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

• 06D30
• 08A05
• 03B35

#### MML

• identifier: NELSON_1
• version: 8.1.045.32.1237
Open Access

Published Online: 13 Aug 2015
Page range: 127 - 160

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

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.

#### Keywords

• subgroup
• Lagrange theorem
• conjugation
• normal subgroup
• index
• basis
• neighborhood