<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, semiring and semialgebra of sets are formalized so as to construct a measure of a given set in the next step. Although a semiring of sets has already been formalized in [13], that is, strictly speaking, a definition of a quasi semiring of sets suggested in the last few decades [15]. We adopt a classical definition of a semiring of sets here to avoid such a confusion. Ring of sets and algebra of sets have been formalized as non empty preboolean set [23] and field of subsets [18], respectively. In the second section, definitions of a ring and a σ-ring of sets, which are based on a semiring and a ring of sets respectively, are formalized and their related theorems are proved. In the third section, definitions of an algebra and a σ-algebra of sets, which are based on a semialgebra and an algebra of sets respectively, are formalized and their related theorems are proved. In the last section, mutual relationships between σ-ring and σ-algebra of sets are formalized and some related examples are given. The formalization is based on [15], and also referred to [9] and [16].</p></abstract>

In this article, semiring and semialgebra of sets are formalized so as to construct a measure of a given set in the next step. Although a semiring of sets has already been formalized in [13], that is, strictly speaking, a definition of a quasi semiring of sets suggested in the last few decades [15]. We adopt a classical definition of a semiring of sets here to avoid such a confusion. Ring of sets and algebra of sets have been formalized as non empty preboolean set [23] and field of subsets [18], respectively. In the second section, definitions of a ring and a σ-ring of sets, which are based on a semiring and a ring of sets respectively, are formalized and their related theorems are proved. In the third section, definitions of an algebra and a σ-algebra of sets, which are based on a semialgebra and an algebra of sets respectively, are formalized and their related theorems are proved. In the last section, mutual relationships between σ-ring and σ-algebra of sets are formalized and some related examples are given. The formalization is based on [15], and also referred to [9] and [16].

σ-ring and σ-algebra of Sets<xref ref-type="fn" rid="fn1_w2aab2b8b8b1b7b1ab1aaAa"><sup>1</sup></xref>

Gifu National College of Technology, Gifu, Japan

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

In this article, semiring and semialgebra of sets are formalized so as to construct a measure of a given set in the next step. Although a semiring of sets has...

σ-ring and σ-algebra of Sets¹

Published Online: Mar 31, 2015

Page range: 51 - 57

Received: Feb 18, 2015

DOI: https://doi.org/10.2478/forma-2015-0004

Keywords
semiring of sets, σ-ring of sets, σ-algebra of sets

© Noboru Endou et al.

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

σ-ring and σ-algebra of Sets1

Published Online: Mar 31, 2015

Page range: 51 - 57

Received: Feb 18, 2015

DOI: https://doi.org/10.2478/forma-2015-0004

Keywordssemiring of sets, σ-ring of sets, σ-algebra of sets

© Noboru Endou et al.

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.

σ-ring and σ-algebra of Sets¹

Keywords
semiring of sets, σ-ring of sets, σ-algebra of sets