A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Andrzej Owsiejczuk.
Combinatorial Grassmannians,
Formalized Mathematics 15(2),
pages 27-33, 2007. MML Identifier: COMBGRAS Summary: In the paper I construct the configuration $G$ which is a partial linear space.
It consists of $k$-element subsets of some base set as points and $(k+1)$-element subsets as lines.
The incidence is given by inclusion. I also introduce automorphisms of partial linear
spaces and show that automorphisms of $G$ are generated by permutations of the base set.
Marco Riccardi.
The Jordan-H\"older Theorem,
Formalized Mathematics 15(2),
pages 35-51, 2007. MML Identifier: GROUP_9 Summary: The goal of this article is to formalize the Jordan-H\"older theorem in the
context of group with operators as in the book \cite{BourbakiAlgI}. Accordingly, the article
introduces the structure of group with operators and reformulates some theorems on a group
already present in the Mizar Mathematical Library. Next, the article formalizes the
Zassenhaus butterfly lemma and the Schreier refinement theorem, and defines the composition series.
Micha{\l} Trybulec.
Regular Expression Quantifiers -- m to n Occurrences,
Formalized Mathematics 15(2),
pages 53-58, 2007. MML Identifier: FLANG_2 Summary: This article includes proofs of several facts that are supplemental to the
theorems proved in \cite{FLANG_1.ABS}. Next, it builds upon that theory to extend the
framework for proving facts about formal languages in general and regular expression
operators in particular. In this article, two quantifiers are defined and their properties
are shown: $m$ to $n$ occurrences (or the union of a range of powers) and optional occurrence.
Although optional occurrence is a special case of the previous operator (0 to 1 occurrences),
it is often defined in regex applications as a separate operator -- hence its explicit definition
and properties in the article. Notation and terminology were taken from \cite{WALL-CHRISTIANSEN-ORWANT:2000}.
Yasunari Shidama, Noboru Endou, Katsumi Wasaki.
Riemann Indefinite Integral of Functions
of Real Variable,
Formalized Mathematics 15(2),
pages 59-63, 2007. MML Identifier: INTEGRA7 Summary: In this article we define the Riemann indefinite integral of functions
of real variable and prove the linearity of that \cite{Apostol:1969}. And we give some
examples of the indefinite integral of some elementary functions. Furthermore, also the
theorem about integral operation and uniform convergent sequence of functions is proved.
Noboru Endou, Yasunari Shidama, Keiichi Miyajima.
Partial Differentiation on Normed Linear
Spaces ${\cal R}^n$,
Formalized Mathematics 15(2),
pages 65-72, 2007. MML Identifier: PDIFF_1 Summary: In this article, we define the partial differentiation of functions of
real variable and prove the linearity of this operator \cite{Schwartz:1981}.