Hiroyuki Okazaki, Noboru Endou, Keiko Narita, Yasunari Shidama.
Differentiable Functions into Real Normed Spaces,
Formalized Mathematics 19(2),
pages 69-72, 2011. MML Identifier:
NDIFF_3 Summary:
In this article, we formalize the differentiability of functions from the set of real numbers into a
normed vector space \cite{CA}.
Robin Nittka.
Conway's Games and Some of their Basic Properties,
Formalized Mathematics 19(2),
pages 73-81, 2011. MML Identifier:
CGAMES_1 Summary:
We formulate a few basic concepts of J.\ H.\ Conway's theory of games based on his
book~\cite{Conway:2001}.
This is a first step towards formalizing Conway's theory of
numbers into Mizar, which is an approach to proving the existence of a FIELD (i.e., a
proper class that satisfies the axioms of a real-closed field) that includes the reals
and ordinals, thus providing a uniform, independent and simple approach to these two
constructions that does not go via the rational numbers and hence does for example not
need the notion of a quotient field.\par In this first article on Conway's games, we
provide a definition of games, their birthdays (or ranks), their trees (a notion which
is not in Conway's book, but is useful as a tool), their negates and their signs, together
with some elementary properties of these notions. If one is interested only in Conway's
numbers, it would have been easier to define them directly, but going via the notion of
a game is a more general approach in the sense that a number is a special instance of a
game and that there is a rich theory of games that are not numbers.\par The main obstacle
in formulating these topics in Mizar is that all definitions are highly recursive, which is
not entirely simple to translate into the Mizar language. For example, according to Conway's
definition, a game is an object consisting of left and right options which are themselves
games, and this is by definition the only way to construct a game. This cannot directly be
translated into Mizar, but a theorem is included in the article which proves that our
definition is equivalent to Conway's.
Grzegorz Bancerek.
Veblen Hierarchy,
Formalized Mathematics 19(2),
pages 83-92, 2011. MML Identifier:
ORDINAL6 Summary:
The Veblen hierarchy is an extension of the construction of epsilon numbers
(fixpoints of the exponential map: $\omega^\epsilon = \epsilon$). It is a
collection $\varphi_\alpha$ of the Veblen Functions
where $\varphi_0(\beta) = \omega^\beta$ and $\varphi_1(\beta) = \epsilon_\beta$.
The sequence of fixpoints of $\varphi_1$ function form $\varphi_2$, etc.
For a limit non empty ordinal $\lambda$ the function $\varphi_\lambda$ is the
sequence of common fixpoints of all functions $\varphi_\alpha$ where $\alpha < \lambda$.\par
The Mizar formalization of the concept cannot be done directly as the Veblen functions are
classes (not (small) sets). It is done with use of universal sets (Tarski classes).
Namely, we define the Veblen functions in a given universal set
and $\varphi_\alpha(\beta)$ as a value of Veblen function from the smallest universal
set including $\alpha$ and $\beta$.
Grzegorz Bancerek.
Sorting by Exchanging,
Formalized Mathematics 19(2),
pages 93-102, 2011. MML Identifier:
EXCHSORT Summary:
We show that exchanging of pairs in an array which are in incorrect order leads to sorted array.
It justifies correctness of Bubble Sort, Insertion Sort, and Quicksort.
Karol P\k{a}k.
{L}inear Transformations of {E}uclidean Topological Spaces,
Formalized Mathematics 19(2),
pages 103-108, 2011. MML Identifier:
MATRTOP1 Summary:
We introduce linear transformations of Euclidean topological spaces given by a transformation
matrix. Next, we prove selected properties and basic arithmetic operations on these linear
transformations. Finally, we show that a linear transformation given by an invertible
matrix is a homeomorphism.
Mariusz Giero.
The Axiomatization of Propositional Linear Time Temporal Logic,
Formalized Mathematics 19(2),
pages 113-119, 2011. MML Identifier:
LTLAXIO1 Summary:
The article introduces propositional linear time temporal logic as a formal system.
Axioms and rules of derivation are defined. Soundness Theorem and Deduction Theorem are
proved \cite{KroMer}.
Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama.
Banach Algebra of Bounded Complex-Valued Functionals,
Formalized Mathematics 19(2),
pages 121-126, 2011. MML Identifier:
CC0SP1 Summary:
In this article, we describe some basic properties of the Banach algebra which is constructed from
all bounded complex-valued functionals.