A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Piotr Rudnicki.
Dilworth's Decomposition Theorem for Posets,
Formalized Mathematics 17(4),
pages 223-232, 2009. MML Identifier:
DILWORTH Summary:
The following theorem is due to Dilworth \cite{Dilworth50}:
Let $P$ be a partially
ordered set. If the maximal number of elements in an independent subset (anti-chain)
of $P$ is $k$, then $P$ is the union of $k$ chains (cliques).\par
In this article we
formalize an elegant proof of the above theorem for finite posets by
Perles \cite{Perles63}.
The result is then used in proving the case of
infinite posets following the original proof of
Dilworth \cite{Dilworth50}.\par
A dual of Dilworth's theorem
also holds: a poset with maximum clique $m$ is a union of $m$ independent sets.
The proof of this dual fact is considerably easier; we follow the proof
by Mirsky \cite{Mirsky71}.
Mirsky states also a corollary
that a poset of $r \times s + 1$ elements possesses a clique of size $r+1$ or
an independent set of size $s+1$, or both. This corollary is then used to prove
the result of Erd\H{o}s and Szekeres \cite{ES35}.\par
Instead of using posets, we drop reflexivity and state the facts about antisymmetric
and transitive relations.
Masahiko Yamazaki, Hiroshi Yamazaki, Katsumi Wasaki, Yasunari Shidama.
Complex Integral,
Formalized Mathematics 17(4),
pages 233-236, 2009. MML Identifier:
INTEGR1C Summary:
In this article, we defined complex curve and complex integral. Then we have proved the
linearity for the complex integral. Furthermore, we have proved complex
integral of complex curve's connection is the sum of each complex integral of individual complex curve.
Adam Grabowski, Magdalena Jastrz\k{e}bska.
On the Lattice of Intervals and Rough Sets,
Formalized Mathematics 17(4),
pages 237-244, 2009. MML Identifier:
INTERVA1 Summary:
Rough sets, developed by Pawlak \cite{Pawlak1982},
are an important tool to describe a situation of incomplete or partially unknown
information. One of the algebraic models deals with the pair of the upper and the
lower approximation. Although usually the tolerance or the equivalence relation is
taken into account when considering a rough set, here we rather concentrate on the
model with the pair of two definable sets, hence we are close to the notion of an interval set.
In this article, the lattices of rough sets and intervals are formalized. This paper,
being essentially the continuation of \cite{ROUGHS_1.ABS},
is also a step towards the
formalization of the algebraic theory of rough sets, as
in \cite{Mousavi:2001}
or \cite{Yao:1993}.
Bo Li, Yanhong Men, Dailu Li, Xiquan Liang.
Basic Properties of Periodic Functions,
Formalized Mathematics 17(4),
pages 245-248, 2009. MML Identifier:
FUNCT_9 Summary:
In this article we present definitions, basic properties and some examples of periodic functions
according to \cite{Chen:1978}.
Grzegorz Bancerek.
Epsilon Numbers and {C}antor Normal Form,
Formalized Mathematics 17(4),
pages 249-256, 2009. MML Identifier:
ORDINAL5 Summary:
An epsilon number is a transfinite number which
is a fixed point of an exponential map: $\omega^\varepsilon = \varepsilon$.
The formalization of the concept is done with use of the tetration
of ordinals
(Knuth's arrow notation, $\uparrow\uparrow$).
Namely, the ordinal indexing of epsilon numbers is defined as follows:
$$\varepsilon_0 = \omega\mathop{\uparrow\uparrow}\omega,\ \ \
\varepsilon_{\alpha+1} = \varepsilon_\alpha\mathop{\uparrow\uparrow}\omega,$
and for limit ordinal $\lambda$:
$$\varepsilon_\lambda = \lim_{\alpha<\lambda}\varepsilon_\alpha
= \bigcup_{\alpha<\lambda}\varepsilon_\alpha.$$
Tetration stabilizes at $\omega$:
$$\alpha\mathop{\uparrow\uparrow}\beta =
\alpha\mathop{\uparrow\uparrow}\omega
\ \ \ {\rm for}\ \ \ \alpha\neq 0\ \ \ {\rm and}\ \ \ \beta\geq\omega.$$
Every ordinal number $\alpha$ can be uniquely written as
$$n_1\omega^{\beta_1} + n_2\omega^{\beta_2} + \cdots + n_k\omega^{\beta_k},$$
where $k$ is a natural number,
$n_1$, $n_2$, $\ldots$, $n_k$ are positive integers,
and $\beta_1 > \beta_2 > \ldots > \beta_k$ are ordinal numbers
($\beta_k = 0$). This decomposition of $\alpha$ is called
the Cantor Normal Form of $\alpha$.