http://hdl.handle.net/11320/4798 2026-06-01T07:20:19Z 2026-06-01T07:20:19Z Coghetto, Roland http://hdl.handle.net/11320/4877 2017-10-05T22:59:24Z 2015-01-01T00:00:00Z

Tytuł: Groups – Additive Notation Autorzy: Coghetto, Roland Abstrakt: AbstractWe translate the articles covering group theory already available in the Mizar Mathematical Library from multiplicative into additive notation. We adapt the works of Wojciech A. Trybulec [41, 42, 43] and Artur Korniłowicz [25]. In particular, these authors have defined the notions of group, abelian group, power of an element of a group, order of a group and order of an element, subgroup, coset of a subgroup, index of a subgroup, conjugation, normal subgroup, topological group, dense subset and basis of a topological group. Lagrange’s theorem and some other theorems concerning these notions [9, 24, 22] are presented. Note that “The term ℤ-module is simply another name for an additive abelian group” [27]. We take an approach different than that used by Futa et al. [21] to use in a future article the results obtained by Artur Korniłowicz [25]. Indeed, Hölzl et al. showed that it was possible to build “a generic theory of limits based on filters” in Isabelle/HOL [23, 10]. Our goal is to define the convergence of a sequence and the convergence of a series in an abelian topological group [11] using the notion of filters.

2015-01-01T00:00:00Z Grabowski, Adam http://hdl.handle.net/11320/4876 2017-10-05T23:09:21Z 2015-01-01T00:00:00Z

Tytuł: Two Axiomatizations of Nelson Algebras Autorzy: Grabowski, Adam Abstrakt: Nelson algebras were first studied by Rasiowa and Białynicki- Birula [1] under the name N-lattices or quasi-pseudo-Boolean algebras. Later, in investigations by Monteiro and Brignole [3, 4], and [2] the name “Nelson algebras” was adopted - which is now commonly used to show the correspondence with Nelson’s paper [14] on constructive logic with strong negation. By a Nelson algebra we mean an abstract algebra 〈L, T, -, ¬, →, ⇒, ⊔, ⊓〉where L is the carrier, − is a quasi-complementation (Rasiowa used the sign ~, but in Mizar “−” should be used to follow the approach described in [12] and [10]), ¬ is a weak pseudo-complementation → is weak relative pseudocomplementation and ⇒ is implicative operation. ⊔ and ⊓ are ordinary lattice binary operations of supremum and infimum. In this article we give the definition and basic properties of these algebras according to [16] and [15]. We start with preliminary section on quasi-Boolean algebras (i.e. de Morgan bounded lattices). Later we give the axioms in the form of Mizar adjectives with names corresponding with those in [15]. As our main result we give two axiomatizations (non-equational and equational) and the full formal proof of their equivalence. The second set of equations is rather long but it shows the logical essence of Nelson lattices. This formalization aims at the construction of algebraic model of rough sets [9] in our future submissions. Section 4 contains all items from Th. 1.2 and 1.3 (and the itemization is given in the text). In the fifth section we provide full formal proof of Th. 2.1 p. 75 [16].

2015-01-01T00:00:00Z Pąk, Karol http://hdl.handle.net/11320/4873 2017-10-05T23:09:20Z 2015-01-01T00:00:00Z

Tytuł: Euler’s Partition Theorem Autorzy: Pąk, Karol Abstrakt: AbstractIn this article we prove the Euler’s Partition Theorem which states that the number of integer partitions with odd parts equals the number of partitions with distinct parts. The formalization follows H.S. Wilf’s lecture notes [28] (see also [1]). Euler’s Partition Theorem is listed as item #45 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/ [27].

2015-01-01T00:00:00Z Coghetto, Roland http://hdl.handle.net/11320/4875 2017-10-05T23:09:21Z 2015-01-01T00:00:00Z

Tytuł: Finite Product of Semiring of Sets Autorzy: Coghetto, Roland Abstrakt: AbstractWe formalize that the image of a semiring of sets [17] by an injective function is a semiring of sets.We offer a non-trivial example of a semiring of sets in a topological space [21]. Finally, we show that the finite product of a semiring of sets is also a semiring of sets [21] and that the finite product of a classical semiring of sets [8] is a classical semiring of sets. In this case, we use here the notation from the book of Aliprantis and Border [1].

2015-01-01T00:00:00Z