Integral of Non Positive Functions
Noboru Endou
Formalized Mathematics, Tome 25 (2017), p. 227-240 / Harvested from The Polish Digital Mathematics Library
Access to full text
Full (PDF)

In this article, we formalize in the Mizar system [1, 7] the Lebesgue type integral and convergence theorems for non positive functions [8],[2]. Many theorems are based on our previous results [5], [6].

Publié le : 2017-01-01
EUDML-ID : urn:eudml:doc:288380 
@article{bwmeta1.element.doi-10_1515_forma-2017-0022,
     author = {Noboru Endou},
     title = {Integral of Non Positive Functions},
     journal = {Formalized Mathematics},
     volume = {25},
     year = {2017},
     pages = {227-240},
     language = {en},
     url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0022}
}

Noboru Endou. Integral of Non Positive Functions. Formalized Mathematics, Tome 25 (2017) pp. 227-240. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0022/