A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Xiquan Liang, Piqing Zhao, Ou Bai.
Vector Functions and their
Differentiation Formulas in 3-dimensional {E}uclidean Spaces,
Formalized Mathematics 18(1),
pages 1-10, 2010. MML Identifier:
EUCLID_8 Summary:
In this article, we first extend several basic theorems of the operation of vector
in 3-dimensional Euclidean spaces. Then three unit vectors: $e1$, $e2$, $e3$ and
the definition of vector function in the same spaces are introduced. By dint of
unit vector the main operation properties as well as the differentiation formulas
of vector function are shown \cite{Spiegel:1959}.
Katuhiko Kanazashi, Noboru Endou, Yasunari Shidama.
Banach Algebra of Continuous
Functionals and the Space of Real-Valued Continuous Functionals with Bounded
Support,
Formalized Mathematics 18(1),
pages 11-16, 2010. MML Identifier:
C0SP2 Summary:
In this article, we give a definition
of a functional space which is constructed from all continuous
functions defined on a compact topological
space. We prove that this functional space is a Banach algebra.
Next, we give a definition of a function space
which is constructed from all real-valued continuous functions
with bounded support. We prove that this
function space is a real normed space.
Marco Riccardi.
Free Magmas,
Formalized Mathematics 18(1),
pages 17-26, 2010. MML Identifier:
ALGSTR_4 Summary:
This article introduces the free magma $M(X)$ constructed on a set
$X$ \cite{BourbakiAlgI}.
Then, we formalize some theorems about $M(X)$:
if $f$ is a function from the set $X$ to a magma $N$, the free magma $M(X)$
has a unique extension of $f$ to a morphism of $M(X)$ into $N$ and every
magma is isomorphic to a magma generated by a set $X$ under a set of relators
on $M(X)$. In doing it, the article defines the stable subset under the law of
composition of a magma, the submagma, the equivalence relation compatible with
the law of composition and the equivalence kernel of a function. We also introduce
some schemes on the recursive function.
Bo Li, Na Ma.
Integrability Formulas. {P}art {I},
Formalized Mathematics 18(1),
pages 27-37, 2010. MML Identifier:
INTEGR12 Summary:
In this article, we give several differentiation and integrability formulas
of special and composite functions including the trigonometric function,
and the polynomial function.
Takao Inou\'e, Bing Xie, Xiquan Liang.
Partial Differentiation of Real Ternary Functions,
Formalized Mathematics 18(1),
pages 39-46, 2010. MML Identifier:
PDIFF_4 Summary:
In this article, we shall extend the result
of \cite{PDIFF_2.ABS}
to discuss partial differentiation of real ternary functions
(refer to \cite{PDIFF_1.ABS}
and \cite{Rudin:1976}
for partial differentiation).
Kazuhisa Ishida, Yasunari Shidama.
Fixpoint Theorem for Continuous Functions on Chain-Complete Posets,
Formalized Mathematics 18(1),
pages 47-51, 2010. MML Identifier:
POSET_1 Summary:
This text includes the definition of chain-complete poset, fix-point
theorem on it, and the definition of the function space of continuous
functions on chain-complete
posets \cite{Winskel:1993}.
Dailu Li, Xiquan Liang, Yanhong Men.
Nilpotent Groups,
Formalized Mathematics 18(1),
pages 53-56, 2010. MML Identifier:
GRNILP_1 Summary:
This article describes the concept of the nilpotent group and some properties of the nilpotent groups.
Xiquan Liang, Ling Tang.
Difference and Difference Quotient. {P}art {III},
Formalized Mathematics 18(1),
pages 57-64, 2010. MML Identifier:
DIFF_3 Summary:
In this article, we give some important theorems of forward difference,
backward difference, central difference and difference quotient
and forward difference, backward difference, central difference
and difference quotient formulas of some special functions.
Grzegorz Bancerek.
A Model of {M}izar Concepts -- Unification,
Formalized Mathematics 18(1),
pages 65-75, 2010. MML Identifier:
ABCMIZ_A Summary:
The aim of this paper is to develop a formal theory of Mizar linguistic
concepts following the ideas
from \cite{Bancerek:2003}
and \cite{ABCMIZ_1.ABS}.
The theory presented is an abstraction from the existing implementation
of the Mizar system and is devoted to the formalization of Mizar expressions.
The concepts formalized here are: standarized constructor signature,
arity-rich signatures, and the unification of Mizar expressions.
Karol P\k{a}k.
Affine Independence in Vector Spaces,
Formalized Mathematics 18(1),
pages 87-93, 2010. MML Identifier:
RLAFFIN1 Summary:
In this article we describe the notion of affinely independent subset of a
real linear space. First we prove selected theorems concerning operations
on linear combinations. Then we introduce affine independence and prove the
equivalence of various definitions of this notion. We also introduce the notion
of the affine hull, i.e. a subset generated by a set of vectors which is an
intersection of all affine sets including the given set. Finally, we introduce
and prove selected properties of the barycentric coordinates.
Karol P\k{a}k.
Abstract Simplicial Complexes,
Formalized Mathematics 18(1),
pages 95-106, 2010. MML Identifier:
SIMPLEX0 Summary:
In this article we define the notion of abstract simplicial complexes
and operations on them. We introduce the following basic notions: simplex,
face, vertex, degree, skeleton, subdivision and substructure, and prove some
of their properties.