A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Yasushige Watase, Noboru Endou, Yasunari Shidama.
On ${L}^p$ Space Formed by Real-Valued Partial Functions,
Formalized Mathematics 18(3),
pages 159-169, 2010. MML Identifier:
LPSPACE2 Summary:
This article is the continuation
of \cite{LPSPACE1.ABS}.
We define the set
of $L^p$ integrable functions -- the set of all partial functions whose
absolute value raised to the $p$-th power is integrable. We show that $L^p$
integrable functions form the $L^p$ space. We also prove Minkowski's
inequality, H\"{o}lder's inequality and that $L^p$ space is Banach space
(\cite{Halmos74},
\cite{Rudin:2}).
Artur Korni{\l}owicz.
Miscellaneous Facts about Open Functions and Continuous Functions,
Formalized Mathematics 18(3),
pages 171-174, 2010. MML Identifier:
TOPS_4 Summary:
In this article we give definitions of open functions and continuous functions
formulated in terms of ``balls" of given topological spaces.
Artur Korni{\l}owicz.
On the Continuity of Some Functions,
Formalized Mathematics 18(3),
pages 175-183, 2010. MML Identifier:
TOPREALC Summary:
We prove that basic arithmetic operations preserve continuity of functions.
Karol P\k{a}k.
The Geometric Interior in Real Linear Spaces,
Formalized Mathematics 18(3),
pages 185-188, 2010. MML Identifier:
RLAFFIN2 Summary:
We introduce the notions of the geometric interior and the centre of mass
for subsets of real linear spaces. We prove a number of theorems concerning
these notions which are used in the theory of abstract simplicial complexes.