A note on the Souslin operations
A Remark on Semiproductive Sets.
Banach’s Continuous Inverse Theorem and Closed Graph Theorem
In this article we formalize one of the most important theorems of linear operator theory - the Closed Graph Theorem commonly used in a standard text book such as [10] in Chapter 24.3. It states that a surjective closed linear operator between Banach spaces is bounded.
“Disorder” in lattices of binumerations
Ein algebraischer Beweis für das Church-Rosser-Theorem.
Eine beweistheoretische Anwendung partieller stetiger Funktionale.
Independent instances for some undecidable problems
Le théorème de Karp-Myhill comme corollaire du théorème des mariages Divers aspects de la « non-généralisation » du théorème de Karp-Myhill
On a relationship between countable functionals and projective trees
On certain decompositions of Gödel numberings.
On changes of input/output coding. I.
On changes of input/output coding. II.
On computable real functions
On L 1 Space Formed by Complex-Valued Partial Functions
In this article, we formalized L1 space formed by complexvalued partial functions [11], [15]. The real-valued case was formalized in [22] and this article is its generalization.
On L 1 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 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...
On L p Space Formed by Real-Valued Partial Functions
This article is the continuation of [31]. We define the set of Lp integrable functions - the set of all partial functions whose absolute value raised to the p-th power is integrable. We show that Lp integrable functions form the Lp space. We also prove Minkowski's inequality, Hölder's inequality and that Lp space is Banach space ([15], [27]).
Partial countable and finite functionals.
Propositional extensions of [Book]
Recursive Arithmetic of Skolem II.
Regressive sets of order n.