<abstract xml:lang="en" xmlns="http://www.w3.org/1999/xhtml"><p>Based on [16], authors formalized the integral of an extended real valued measurable function in [12] before. However, the integral argued in [12] cannot be applied to real-valued functions unconditionally. Therefore, in this article we have formalized the integral of a real-value function.</p></abstract>

Based on [16], authors formalized the integral of an extended real valued measurable function in [12] before. However, the integral argued in [12] cannot be applied to real-valued functions unconditionally. Therefore, in this article we have formalized the integral of a real-value function.

Integral of Real-Valued Measurable Function<sup>1</sup>

Gifu National College of Technology, Gifu, Japan

Formalized Mathematics

Integral of Real-Valued Measurable Function

{"article-title":{"content":"Integral of Real-Valued Measurable Function","sup":1}}

Based on [16], authors formalized the integral of an extended real valued measurable function in [12] before. However, the integral argued in [12] cannot be...

Integral of Real-Valued Measurable Function¹

Publié en ligne: 13 juin 2008

Pages: 143 - 152

DOI: https://doi.org/10.2478/v10037-006-0018-8

This content is open access.

Integral of Real-Valued Measurable Function1

Publié en ligne: 13 juin 2008

Pages: 143 - 152

DOI: https://doi.org/10.2478/v10037-006-0018-8

This content is open access.

Integral of Real-Valued Measurable Function¹