<abstract xmlns="http://www.w3.org/1999/xhtml"><p> 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. </p></abstract>

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.

Product Pre-Measure

Gifu National College of Technology Gifu, Japan

Formalized Mathematics

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

{"article-title":"Product Pre-Measure"}

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...

Product Pre-Measure

Pubblicato online: 31 ago 2016

Pagine: 69 - 79

Ricevuto: 31 dic 2015

DOI: https://doi.org/10.1515/forma-2016-0006

Parole chiave
product measure, pre-measure

© by Noboru Endou

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

Product Pre-Measure

Pubblicato online: 31 ago 2016

Pagine: 69 - 79

Ricevuto: 31 dic 2015

DOI: https://doi.org/10.1515/forma-2016-0006

Parole chiaveproduct measure, pre-measure

© by Noboru Endou

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

Parole chiave
product measure, pre-measure