The search session has expired. Please query the service again.
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...
Category theory was formalized in Mizar with two different approaches [7], [18] that correspond to those most commonly used [16], [5]. Since there is a one-to-one correspondence between objects and identity morphisms, some authors have used an approach that does not refer to objects as elements of the theory, and are usually indicated as object-free category [1] or as arrowsonly category [16]. In this article is proposed a new definition of an object-free category, introducing the two properties:...
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.
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.
The first four sections of this article include some auxiliary theorems related to number and finite sequence of numbers, in particular a primality test, the Pocklington's theorem (see [19]). The last section presents the formalization of Bertrand's postulate closely following the book [1], pp. 7-9.
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
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...
This article introduces the definition of n-locally Euclidean topological spaces and topological manifolds [13].
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
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].
In this article, the principal n-th root of a complex number is defined, the Vieta's formulas for polynomial equations of degree 2, 3 and 4 are formalized. The solution of quadratic equations, the Cardan's solution of cubic equations and the Descartes-Euler solution of quartic equations in terms of their complex coefficients are also presented [5].
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.
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].
Triviality of fundamental groups of spheres of dimension greater than 1 is proven, [17]
The Borsuk-Ulam theorem about antipodals is proven, [18, pp. 32-33].
Download Results (CSV)