Xiquan Liang, Dailu Li.
Some Properties of $p$-Groups and Commutative $p$-Groups,
Formalized Mathematics 19(1),
pages 11-15, 2011. MML Identifier:
GROUPP_1 Summary:
This article describes some properties of $p$-groups and some properties of commutative $p$-groups.
Keiichi Miyajima, Takahiro Kato, Yasunari Shidama.
Riemann Integral of Functions from $\mathbb{R}$ into Real Normed Space,
Formalized Mathematics 19(1),
pages 17-22, 2011. MML Identifier:
INTEGR18 Summary:
In this article, we define the Riemann integral on functions from $\mathbb R$
into real normed space and prove the linearity of
this operator. As a result, the Riemann integration can be applied to a wider
range of functions. The proof method follows the \cite{Murray:1974}.
Hiroyuki Okazaki, Kenichi Arai, Yasunari Shidama.
Normal Subgroup of Product of Groups,
Formalized Mathematics 19(1),
pages 23-26, 2011. MML Identifier:
GROUP_12 Summary:
In \cite{GROUP_7.ABS}
it was formalized that the direct product of a family of groups
gives a new group. In this article, we formalize that for all $j \in I$, the
group $G =\Pi_{i \in I} G_i$ has a normal subgroup isomorphic to $G_j$. Moreover,
we show some relations between a family of groups and its direct product.
Piotr Rudnicki, Lorna Stewart.
{T}he {M}ycielskian of a Graph,
Formalized Mathematics 19(1),
pages 27-34, 2011. MML Identifier:
MYCIELSK Summary:
Let $\omega(G)$ and $\chi(G)$ be the clique number and the chromatic number of a
graph $G$. Mycielski~\cite{Mycielski55} presented a construction that for any $n$
creates a graph $M_n$ which is triangle-free ($\omega(G) = 2$) with $\chi(G) > n$.
The starting point is the complete graph of two vertices ($K_2$). $M_{(n+1)}$ is
obtained from $M_n$ through the operation $\mu(G)$ called the Mycielskian of a
graph $G$. \par We first define the operation $\mu(G)$ and then show
that $\omega(\mu(G)) = \omega(G)$ and $\chi(\mu(G)) = \chi(G)+1$. This is done
for arbitrary graph $G$, see also~\cite{LUP95}.
Then we define the sequence of
graphs $M_n$ each of exponential size in $n$ and give their clique and chromatic numbers.
Xiquan Liang, Ling Tang, Xichun Jiang.
{D}ifference and Difference Quotient. {P}art {IV},
Formalized Mathematics 19(1),
pages 35-39, 2011. MML Identifier:
DIFF_4 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.
Marco Riccardi.
The Definition of Topological Manifolds,
Formalized Mathematics 19(1),
pages 41-44, 2011. MML Identifier:
MFOLD_1 Summary:
This article introduces the definition of $n$-locally Euclidean topological spaces
and topological manifolds \cite{JLee2000}.
Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama.
More on Continuous Functions on Normed Linear Spaces,
Formalized Mathematics 19(1),
pages 45-49, 2011. MML Identifier:
NFCONT_3 Summary:
In this article we formalize the definition and some facts about continuous functions from $\Bbb R$ into
normed linear spaces \cite{Schwartz:1967}.
Hiroyuki Okazaki, Noboru Endou, Yasunari Shidama.
Cartesian Products of Family of Real Linear Spaces,
Formalized Mathematics 19(1),
pages 51-59, 2011. MML Identifier:
PRVECT_3 Summary:
In this article we introduced the isomorphism mapping between cartesian products
of family of linear spaces \cite{BOURBAKI:1-5}.
Those products had been formalized
by two different ways, i.e., the way using the functor [:X,Y:] and ones using the
functor ``product". By the same way, the isomorphism mapping was defined between
Cartesian products of family of linear normed spaces also.
Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama.
Formalization of Integral Linear Space,
Formalized Mathematics 19(1),
pages 61-64, 2011. MML Identifier:
RLVECT_X Summary:
In this article, we formalize integral linear spaces, that is a linear space with
integer coefficients. Integral linear spaces are necessary for lattice problems,
LLL (Lenstra-Lenstra-Lov\'{a}sz) base reduction algorithm
that outputs short lattice base and cryptographic systems with
lattice~\cite{Micci:2002}.