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

Full description

Bibliographic Details
Main Author: Endou Noboru
Format: Article
Language:English
Published: Sciendo 2016-03-01
Series:Formalized Mathematics
Subjects:
Online Access:https://doi.org/10.1515/forma-2016-0006