Commutativeness of Fundamental Groups of Topological Groups
In this article we prove that fundamental groups based at the unit point of topological groups are commutative [11].
Miscellaneous Facts about Open Functions and Continuous Functions
In this article we give definitions of open functions and continuous functions formulated in terms of "balls" of given topological spaces.
Collective Operations on Number-Membered Sets
The article starts with definitions of sets of opposite and inverse numbers of a given number membered set. Next, collective addition, subtraction, multiplication and division of two sets are defined. Complex numbers cases and extended real numbers ones are introduced separately and unified for reals. Shortcuts for singletons cases are also defined.
The Correspondence Between n -dimensional Euclidean Space and the Product of n Real Lines
In the article we prove that a family of open n-hypercubes is a basis of n-dimensional Euclidean space. The equality of the space and the product of n real lines has been proven.
Cayley's Theorem
The article formalizes the Cayley's theorem saying that every group G is isomorphic to a subgroup of the symmetric group on G.
Cayley-Dickson Construction
Cayley-Dickson construction produces a sequence of normed algebras over real numbers. Its consequent applications result in complex numbers, quaternions, octonions, etc. In this paper we formalize the construction and prove its basic properties.
Arithmetic Operations on Functions from Sets into Functional Sets
In this paper we introduce sets containing number-valued functions. Different arithmetic operations on maps between any set and such functional sets are later defined.MML identifier: VALUED 2, version: 7.11.01 4.117.1046
On the Continuity of Some Functions
We prove that basic arithmetic operations preserve continuity of functions.
Mazur-Ulam Theorem
The Mazur-Ulam theorem [15] has been formulated as two registrations: cluster bijective isometric -> midpoints-preserving Function of E, F; and cluster isometric midpoints-preserving -> Affine Function of E, F; A proof given by Jussi Väisälä [23] has been formalized.
Products in Categories without Uniqueness of cod and dom
The paper introduces Cartesian products in categories without uniqueness of cod and dom. It is proven that set-theoretical product is the product in the category Ens [7].
Differentiability of Polynomials over Reals
In this article, we formalize in the Mizar system [3] the notion of the derivative of polynomials over the field of real numbers [4]. To define it, we use the derivative of functions between reals and reals [9].
Coproducts in Categories without Uniqueness of cod and dom
The paper introduces coproducts in categories without uniqueness of cod and dom. It is proven that set-theoretical disjoint union is the coproduct in the category Ens [9].
The First Isomorphism Theorem and Other Properties of Rings
Different properties of rings and fields are discussed [12], [41] and [17]. We introduce ring homomorphisms, their kernels and images, and prove the First Isomorphism Theorem, namely that for a homomorphism f : R → S we have R/ker(f) ≅ Im(f). Then we define prime and irreducible elements and show that every principal ideal domain is factorial. Finally we show that polynomial rings over fields are Euclidean and hence also factorial
Basic Operations on Preordered Coherent Spaces
This Mizar paper presents the definition of a "Preordered Coherent Space" (PCS). Furthermore, the paper defines a number of operations on PCS's and states and proves a number of elementary lemmas about these operations. PCS's have many useful properties which could qualify them for mathematical study in their own right. PCS's were invented, however, to construct Scott domains, to solve domain equations, and to construct models of various versions of lambda calculus.For more on PCS's, see [11]. The...
Fundamental Group of n-sphere for n ≥ 2
Triviality of fundamental groups of spheres of dimension greater than 1 is proven, [17]
The Borsuk-Ulam Theorem
The Borsuk-Ulam theorem about antipodals is proven, [18, pp. 32-33].
Basel Problem
A rigorous elementary proof of the Basel problem [6, 1] ∑n=1∞1n2=π26 is formalized in the Mizar system [3]. This theorem is item 14 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.
Basel Problem – Preliminaries
In the article we formalize in the Mizar system [4] preliminary facts needed to prove the Basel problem [7, 1]. Facts that are independent from the notion of structure are included here.
Vieta’s Formula about the Sum of Roots of Polynomials
In the article we formalized in the Mizar system [2] the Vieta formula about the sum of roots of a polynomial anxn + an−1xn−1 + ··· + a1x + a0 defined over an algebraically closed field. The formula says that [...] x1+x2+⋯+xn−1+xn=−an−1an , where x1, x2,…, xn are (not necessarily distinct) roots of the polynomial [12]. In the article the sum is denoted by SumRoots.
Introduction to Liouville Numbers
The article defines Liouville numbers, originally introduced by Joseph Liouville in 1844 [17] as an example of an object which can be approximated “quite closely” by a sequence of rational numbers. A real number x is a Liouville number iff for every positive integer n, there exist integers p and q such that q > 1 and [...] It is easy to show that all Liouville numbers are irrational. Liouville constant, which is also defined formally, is the first transcendental (not algebraic) number. It is...
Page 1 Next