A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Karol P\k{a}k.
Sperner's Lemma,
Formalized Mathematics 18(4),
pages 189-196, 2010. MML Identifier:
SIMPLEX1 Summary:
In this article we introduce and prove properties of simplicial complexes in
real linear spaces which are necessary to formulate Sperner's lemma. The lemma
states that for a function $f$, which for an arbitrary vertex $v$ of the
barycentric subdivision $\mathcal{B}$ of simplex $\mathcal{K}$ assigns some
vertex from a face of $\mathcal{K}$ which contains $v$, we can find a
simplex $S$ of $\mathcal{B}$ which satisfies $f(S)=\mathcal{K}$
(see \cite{DUDA:BM61}).
Cezary Kaliszyk.
Counting Derangements, Non Bijective Functions and the Birthday Problem,
Formalized Mathematics 18(4),
pages 197-200, 2010. MML Identifier:
CARDFIN2 Summary:
The article provides counting derangements of finite sets
and counting non bijective functions. We provide a recursive formula
for the number of derangements of a finite set, together with an
explicit formula involving the number $e$. We count the number of
non-one-to-one functions between to finite sets and perform a computation
to give explicitely a formalization of the birthday problem. The article
is an extension of \cite{CARD_FIN.ABS}.
Keiichi Miyajima, Takahiro Kato, Yasunari Shidama.
Riemann Integral of Functions $\mathbb{R}$ into $\mathbb{C}$,
Formalized Mathematics 18(4),
pages 201-206, 2010. MML Identifier:
INTEGR16 Summary:
In this article, we define the Riemann Integral on functions $\mathbb{R}$
into $\mathbb{C}$ and proof the linearity of this operator. Especially,
the Riemann integral of complex functions is constituted by the redefinition
about the Riemann sum of complex numbers. Our method refers to
the \cite{Murray:1974}.
Hiroyuki Okazaki, Yasunari Shidama.
{P}robability Measure on Discrete Spaces
and Algebra of Real-Valued Random Variables,
Formalized Mathematics 18(4),
pages 213-217, 2010. MML Identifier:
RANDOM_2 Summary:
In this article we continue formalizing probability and randomness started
in \cite{RANDOM_1.ABS},
where we formalized some theorems concerning the probability and real-valued
random variables. In this paper we formalize the variance of a random variable
and prove Chebyshev's inequality. Next we formalize the product probability
measure on the Cartesian product of discrete spaces. In the final part of
this article we define the algebra of real-valued random variables.