<abstract xml:lang="en" xmlns="http://www.w3.org/1999/xhtml">This article contains some definitions and properties refering to function spaces formed by partial functions defined over a measurable space. We formalized a function space, the so-called <italic>L</italic>1 space and proved that the space turns out to be a normed space. The formalization of a real function space was given in [16]. The set of all function forms additive group. Here addition is defined by point-wise addition of two functions. However it is not true for partial functions. The set of partial functions does not form an additive group due to lack of right zeroed condition. Therefore, firstly we introduced a kind of a quasi-linear space, then, we introduced the definition of an equivalent relation of two functions which are almost everywhere equal (=a.e.), thirdly we formalized a linear space by taking the quotient of a quasi-linear space by the relation (=a.e.).MML identifier: LPSPACE1, version: 7.9.03 4.108.1028</abstract>

This article contains some definitions and properties refering to function spaces formed by partial functions defined over a measurable space. We formalized a function space, the so-called L1 space and proved that the space turns out to be a normed space. The formalization of a real function space was given in [16]. The set of all function forms additive group. Here addition is defined by point-wise addition of two functions. However it is not true for partial functions. The set of partial functions does not form an additive group due to lack of right zeroed condition. Therefore, firstly we introduced a kind of a quasi-linear space, then, we introduced the definition of an equivalent relation of two functions which are almost everywhere equal (=a.e.), thirdly we formalized a linear space by taking the quotient of a quasi-linear space by the relation (=a.e.).MML identifier: LPSPACE1, version: 7.9.03 4.108.1028

On <italic>L</italic>1 Space Formed by Real-Valued Partial Functions

Gifu National College of Technology, Japan

Formalized Mathematics

On  Space Formed by Real-Valued Partial Functions

This article contains some definitions and properties refering to function spaces formed by partial functions defined over a measurable space. We formalized a...

On L¹ Space Formed by Real-Valued Partial Functions

Online veröffentlicht: 20. März 2009

Seitenbereich: 361 - 369

DOI: https://doi.org/10.2478/v10037-008-0044-9

This content is open access.

On L1 Space Formed by Real-Valued Partial Functions

Online veröffentlicht: 20. März 2009

Seitenbereich: 361 - 369

DOI: https://doi.org/10.2478/v10037-008-0044-9

This content is open access.

On L¹ Space Formed by Real-Valued Partial Functions