On L¹ Space Formed by Complex-Valued Partial Functions

In this article, we formalized L¹ space formed by complexvalued partial functions [11], [15]. The real-valued case was formalized in [22] and this article is its generalization.