O artykule
Data publikacji: 31 sie 2016
Zakres stron: 69 - 79
Otrzymano: 31 gru 2015
DOI: https://doi.org/10.1515/forma-2016-0006
Słowa kluczowe
© by Noboru Endou
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License.
In this article we formalize in Mizar [5] product pre-measure on product sets of measurable sets. Although there are some approaches to construct product measure [22], [6], [9], [21], [25], we start it from σ-measure because existence of σ-measure on any semialgebras has been proved in [15]. In this approach, we use some theorems for integrals.