Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 15

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote

Free Magmas

100%
Riccardi M.
Formalized Mathematics
|
2010
|
tom 18
|
nr 1
17-26
EN
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.
2
Content available remote

Planes and Spheres as Topological Manifolds. Stereographic Projection

100%
Riccardi M.
Formalized Mathematics
|
2012
|
tom 20
|
nr 1
41-45
EN
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].
3
Content available remote

Pocklington's Theorem and Bertrand's Postulate

100%
Riccardi M.
Formalized Mathematics
|
2006
|
tom 14
|
nr 2
47-52
EN
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.
4
Content available remote

The Perfect Number Theorem and Wilson's Theorem

100%
Riccardi M.
Formalized Mathematics
|
2009
|
tom 17
|
nr 2
123-128
EN
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.
5
Content available remote

The Sylow Theorems

100%
Riccardi M.
Formalized Mathematics
|
2007
|
tom 15
|
nr 3
159-165
EN
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.
6
Content available remote

Solution of Cubic and Quartic Equations

100%
Riccardi M.
Formalized Mathematics
|
2009
|
tom 17
|
nr 2
117-122
EN
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].
7
Content available remote

Categorical Pullbacks

100%
Riccardi M.
Formalized Mathematics
|
2015
|
tom 23
|
nr 1
1-14
EN
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].
8
Content available remote

The Jordan-Hölder Theorem

100%
Riccardi M.
Formalized Mathematics
|
2007
|
tom 15
|
nr 2
35-51
EN
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.
9
Content available remote

Heron's Formula and Ptolemy's Theorem

100%
Riccardi M.
Formalized Mathematics
|
2008
|
tom 16
|
nr 2
97-101
EN
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
10
Content available remote

The Definition of Topological Manifolds

100%
Riccardi M.
Formalized Mathematics
|
2011
|
tom 19
|
nr 1
41-44
EN
This article introduces the definition of n-locally Euclidean topological spaces and topological manifolds [13].
11
Content available remote

Object-Free Definition of Categories

100%
Riccardi M.
Formalized Mathematics
|
2013
|
tom 21
|
nr 3
193-205
EN
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: left composable and right composable, and a simplification of the notation through a symbol, a binary relation between morphisms, that indicates whether the composition is defined. In the final part we define two functions that allow to switch from the two definitions, with and without objects, and it is shown that their composition produces isomorphic categories.
12
Content available remote

Exponential Objects

100%
Riccardi M.
Formalized Mathematics
|
2015
|
tom 23
|
nr 4
351-369
EN
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].
13
Content available remote

Ramsey's Theorem

100%
Riccardi M.
Formalized Mathematics
|
2008
|
tom 16
|
nr 2
203-205
EN
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
14
Content available remote

The Borsuk-Ulam Theorem

64%
Korniłowicz A., Riccardi M.
Formalized Mathematics
|
2012
|
tom 20
|
nr 2
105-112
EN
The Borsuk-Ulam theorem about antipodals is proven, [18, pp. 32-33].
15
Content available remote

Fundamental Group of n-sphere for n ≥ 2

64%
Riccardi M., Korniłowicz A.
Formalized Mathematics
|
2012
|
tom 20
|
nr 2
97-104
EN
Triviality of fundamental groups of spheres of dimension greater than 1 is proven, [17]
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.