http://hdl.handle.net/11320/5548 2026-06-01T15:15:34Z http://hdl.handle.net/11320/5556 Tytu&#322;: Uniform Space Autorzy: Coghetto, Roland Abstrakt: In this article, we formalize in Mizar [1] the notion of uniform space introduced by André Weil using the concepts of entourages [2].We present some results between uniform space and pseudo metric space. We introduce the concepts of left-uniformity and right-uniformity of a topological group.Next, we define the concept of the partition topology. Following the Vlach’s works [11, 10], we define the semi-uniform space induced by a tolerance and the uniform space induced by an equivalence relation.Finally, using mostly Gehrke, Grigorieff and Pin [4] works, a Pervin uniform space defined from the sets of the form ((X\A) × (X\A)) ∪ (A×A) is presented. 2016-01-01T00:00:00Z http://hdl.handle.net/11320/5557 Tytu&#322;: Some Algebraic Properties of Polynomial Rings Autorzy: Schwarzweller, Christoph; Korniłowicz, Artur; Rowinska-Schwarzweller, Agnieszka Abstrakt: In this article we extend the algebraic theory of polynomial rings, formalized in Mizar [1], based on [2], [3]. After introducing constant and monic polynomials we present the canonical embedding of R into R[X] and deal with both unit and irreducible elements. We also define polynomial GCDs and show that for fields F and irreducible polynomials p the field F[X]/<p> is isomorphic to the field of polynomials with degree smaller than the one of p. 2016-01-01T00:00:00Z http://hdl.handle.net/11320/5553 Tytu&#322;: Prime Factorization of Sums and Differences of Two Like Powers Autorzy: Ziobro, Rafał Abstrakt: Representation of a non zero integer as a signed product of primes is unique similarly to its representations in various types of positional notations [4], [3]. The study focuses on counting the prime factors of integers in the form of sums or differences of two equal powers (thus being represented by 1 and a series of zeroes in respective digital bases).Although the introduced theorems are not particularly important, they provide a couple of shortcuts useful for integer factorization, which could serve in further development of Mizar projects [2]. This could be regarded as one of the important benefits of proof formalization [9]. 2016-01-01T00:00:00Z http://hdl.handle.net/11320/5555 Tytu&#322;: Quasi-uniform Space Autorzy: Coghetto, Roland Abstrakt: In this article, using mostly Pervin [9], Kunzi [6], [8], [7], Williams [11] and Bourbaki [3] works, we formalize in Mizar [2] the notions of quasiuniform space, semi-uniform space and locally uniform space.We define the topology induced by a quasi-uniform space. Finally we formalize from the sets of the form ((X \ Ω) × X) ∪ (X × Ω), the Csaszar-Pervin quasi-uniform space induced by a topological space. 2016-01-01T00:00:00Z