On L 1 Space Formed by Real-Valued Partial Functions
Yasushige Watase, Noboru Endou, Yasunari Shidama (2008)
Formalized Mathematics
Similarity:
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...