Search Results

You are looking at 1 - 10 of 15 items for

  • Author: Marco Riccardi x
Clear All Modify Search
Open access

Marco Riccardi

Planes and Spheres as Topological Manifolds. Stereographic Projection

The goal of this article is to show some examples of topological manifolds: planes and spheres in Euclidean space. In doing it, the article introduces the stereographic projection [25].

Open access

Marco Riccardi

Summary

In the first part of this article we formalize the concepts of terminal and initial object, categorical product [4] and natural transformation within a free-object category [1]. In particular, we show that this definition of natural transformation is equivalent to the standard definition [13]. Then we introduce the exponential object using its universal property and we show the isomorphism between the exponential object of categories and the functor category [12].

Open access

Marco Riccardi

The Sylow Theorems

The goal of this article is to formalize the Sylow theorems closely following the book [4]. Accordingly, the article introduces the group operating on a set, the stabilizer, the orbits, the p-groups and the Sylow subgroups.

Open access

Marco Riccardi

Ramsey's Theorem

The goal of this article is to formalize two versions of Ramsey's theorem. The theorems are not phrased in the usually pictorial representation of a coloured graph but use a set-theoretic terminology. After some useful lemma, the second section presents a generalization of Ramsey's theorem on infinite set closely following the book [9]. The last section includes the formalization of the theorem in a more known version (see [1]).

MML identifier: RAMSEY 1, version: 7.9.01 4.101.1015

Open access

Marco Riccardi

Summary

The main purpose of this article is to introduce the categorical concept of pullback in Mizar. In the first part of this article we redefine homsets, monomorphisms, epimorpshisms and isomorphisms [7] within a free-object category [1] and it is shown there that ordinal numbers can be considered as categories. Then the pullback is introduced in terms of its universal property and the Pullback Lemma is formalized [15]. In the last part of the article we formalize the pullback of functors [14] and it is also shown that it is not possible to write an equivalent definition in the context of the previous Mizar formalization of category theory [8].

Open access

Marco Riccardi

Heron's Formula and Ptolemy's Theorem

The goal of this article is to formalize some theorems that are in the [17] on the web. These are elementary theorems included in every handbook of Euclidean geometry and trigonometry: the law of cosines, the Heron's formula, the isosceles triangle theorem, the intersecting chords theorem and the Ptolemy's theorem.

MML identifier: EUCLID 6, version: 7.8.09 4.97.1001

Open access

Marco Riccardi

The Perfect Number Theorem and Wilson's Theorem

This article formalizes proofs of some elementary theorems of number theory (see [1, 26]): Wilson's theorem (that n is prime iff n > 1 and (n - 1)! ≅ -1 (mod n)), that all primes (1 mod 4) equal the sum of two squares, and two basic theorems of Euclid and Euler about perfect numbers. The article also formally defines Euler's sum of divisors function Φ, proves that Φ is multiplicative and that Σk|n Φ(k) = n.

Open access

Marco Riccardi

Free Magmas

This article introduces the free magma M(X) constructed on a set X [6]. Then, we formalize some theorems about M(X): if f is a function from the set X to a magma N, the free magma M(X) has a unique extension of f to a morphism of M(X) into N and every magma is isomorphic to a magma generated by a set X under a set of relators on M(X). In doing it, the article defines the stable subset under the law of composition of a magma, the submagma, the equivalence relation compatible with the law of composition and the equivalence kernel of a function. We also introduce some schemes on the recursive function.

Open access

Marco Riccardi

The Jordan-Hölder Theorem

The goal of this article is to formalize the Jordan-Hölder theorem in the context of group with operators as in the book [5]. Accordingly, the article introduces the structure of group with operators and reformulates some theorems on a group already present in the Mizar Mathematical Library. Next, the article formalizes the Zassenhaus butterfly lemma and the Schreier refinement theorem, and defines the composition series.

Open access

Marco Riccardi

The Definition of Topological Manifolds

This article introduces the definition of n-locally Euclidean topological spaces and topological manifolds [13].