<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article, we formalize in the Mizar system [<xref ref-type="bibr" rid="j_forma-2017-0022_ref_001_w2aab3b7b6b1b6b1ab1ab1Aa">1</xref>, <xref ref-type="bibr" rid="j_forma-2017-0022_ref_007_w2aab3b7b6b1b6b1ab1ab7Aa">7</xref>] the Lebesgue type integral and convergence theorems for non positive functions [<xref ref-type="bibr" rid="j_forma-2017-0022_ref_008_w2aab3b7b6b1b6b1ab1ab8Aa">8</xref>],[<xref ref-type="bibr" rid="j_forma-2017-0022_ref_002_w2aab3b7b6b1b6b1ab1ab2Aa">2</xref>]. Many theorems are based on our previous results [<xref ref-type="bibr" rid="j_forma-2017-0022_ref_005_w2aab3b7b6b1b6b1ab1ab5Aa">5</xref>], [<xref ref-type="bibr" rid="j_forma-2017-0022_ref_006_w2aab3b7b6b1b6b1ab1ab6Aa">6</xref>].</p></abstract>

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

Integral of Non Positive Functions

Formalized Mathematics

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

{"article-title":"Integral of Non Positive Functions"}

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

Integral of Non Positive Functions

Publicado en línea: 19 dic 2017

Páginas: 227 - 240

Recibido: 03 sept 2017

DOI: https://doi.org/10.1515/forma-2017-0022

Palabras clave
integration of non positive function

© 2017 Noboru Endou, published by De Gruyter Open

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

Integral of Non Positive Functions

Publicado en línea: 19 dic 2017

Páginas: 227 - 240

Recibido: 03 sept 2017

DOI: https://doi.org/10.1515/forma-2017-0022

Palabras claveintegration of non positive function

© 2017 Noboru Endou, published by De Gruyter Open

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

Palabras clave
integration of non positive function