http://hdl.handle.net/11320/3667 Mon, 01 Jun 2026 15:10:26 GMT 2026-06-01T15:10:26Z http://hdl.handle.net/11320/3728 Tytuł: The Formal Construction of Fuzzy Numbers Autorzy: Grabowski, Adam Abstrakt: In this article, we continue the development of the theory of fuzzy sets [23], started with [14] with the future aim to provide the formalization of fuzzy numbers [8] in terms reflecting the current state of the Mizar Mathematical Library. Note that in order to have more usable approach in [14], we revised that article as well; some of the ideas were described in [12]. As we can actually understand fuzzy sets just as their membership functions (via the equality of membership function and their set-theoretic counterpart), all the calculations are much simpler. To test our newly proposed approach, we give the notions of (normal) triangular and trapezoidal fuzzy sets as the examples of concrete fuzzy objects. Also -cuts, the core of a fuzzy set, and normalized fuzzy sets were defined. Main technical obstacle was to prove continuity of the glued maps, and in fact we did this not through its topological counterpart, but extensively reusing properties of the real line (with loss of generality of the approach, though), because we aim at formalizing fuzzy numbers in our future submissions, as well as merging with rough set approach as introduced in [13] and [11]. Our base for formalization was [9] and [10]. Wed, 01 Jan 2014 00:00:00 GMT http://hdl.handle.net/11320/3728 2014-01-01T00:00:00Z http://hdl.handle.net/11320/3727 Tytuł: Some Facts about Trigonometry and Euclidean Geometry Autorzy: Coghetto, Roland Abstrakt: We calculate the values of the trigonometric functions for angles: [XXX] , by [16]. After defining some trigonometric identities, we demonstrate conventional trigonometric formulas in the triangle, and the geometric property, by [14], of the triangle inscribed in a semicircle, by the proposition 3.31 in [15]. Then we define the diameter of the circumscribed circle of a triangle using the definition of the area of a triangle and prove some identities of a triangle [9]. We conclude by indicating that the diameter of a circle is twice the length of the radius. Wed, 01 Jan 2014 00:00:00 GMT http://hdl.handle.net/11320/3727 2014-01-01T00:00:00Z http://hdl.handle.net/11320/3724 Tytuł: Torsion Z-module and Torsion-free Z-module Autorzy: Futa, Yuichi; Okazaki, Hiroyuki; Nakasho, Kazuhisa; Shidama, Yasunari Abstrakt: In this article, we formalize a torsion Z-module and a torsionfree Z-module. Especially, we prove formally that finitely generated torsion-free Z-modules are finite rank free. We also formalize properties related to rank of finite rank free Z-modules. The notion of Z-module is necessary for solving lattice problems, LLL (Lenstra, Lenstra, and Lov´asz) base reduction algorithm [20], cryptographic systems with lattice [21], and coding theory [11]. Wed, 01 Jan 2014 00:00:00 GMT http://hdl.handle.net/11320/3724 2014-01-01T00:00:00Z http://hdl.handle.net/11320/3725 Tytuł: The First Isomorphism Theorem and Other Properties of Rings Autorzy: Korniłowicz, Artur; Schwarzweller, Christoph Abstrakt: 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. Wed, 01 Jan 2014 00:00:00 GMT http://hdl.handle.net/11320/3725 2014-01-01T00:00:00Z