Integral of Non Positive Functions

• Autorzy: Noboru Endou
• Języki publikacji: EN

Abstrakty

EN

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

Słowa kluczowe

EN

integration of non positive function

Kategorie tematyczne

• 03B35: Mechanization of proofs and logical operations
• 28A25: Integration with respect to measures and other set functions

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2017
• Tom: 25
• Numer: 3
• Strony: 227-240

Daty

wydano

2017-10-01

otrzymano

2017-09-03

online

2017-12-19

Twórcy

autor

Noboru Endou

• , , Kamimakuwa, Motosu, ,

Identyfikatory

DOI

10.1515/forma-2017-0022