A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Karol P\k{a}k.
Basic Properties of Metrizable Topological Spaces,
Formalized Mathematics 17(3),
pages 201-205, 2009. MML Identifier:
METRIZTS Summary:
We continue Mizar formalization of general topology according to the book \cite{ENGEL:1} by Engelking.
In the article, we present the final theorem of Section 4.1. Namely, the paper includes the formalization
of theorems on the correspondence between the cardinalities of the basis and of some open subcover,
and a discreet (closed) subspaces, and the weight of that metrizable topological space.
We also define Lindel\"of spaces and state the above theorem in this special case.
We also introduce the concept of separation among two subsets (see \cite{ENGEL:BM51}).
Karol P\k{a}k.
Small Inductive Dimension of Topological Spaces,
Formalized Mathematics 17(3),
pages 207-212, 2009. MML Identifier:
TOPDIM_1 Summary:
We present the concept and basic properties of the Menger-Urysohn small inductive dimension
of topological spaces according to the books \cite{DUDA:BM61}.
Namely, the paper includes
the formalization of main theorems from Sections 1.1 and 1.2.
Xiquan Liang, Dailu Li.
On Rough Subgroup of a Group,
Formalized Mathematics 17(3),
pages 213-217, 2009. MML Identifier:
GROUP_11 Summary:
This article describes a rough subgroup with respect to a normal subgroup of a group,
and some properties of the lower and the upper approximations in a group.
Karol P\k{a}k.
Small Inductive Dimension of Topological Spaces. {P}art {II},
Formalized Mathematics 17(3),
pages 219-222, 2009. MML Identifier:
TOPDIM_2 Summary:
In this paper we present basic properties of $n$-dimensional topological spaces according to the
book \cite{ENGEL:BM51}. In the article the formalization of Section 1.5 is completed.