Formalized Mathematics    (ISSN 1426-2630)
Volume 6, Number 3 (1997): pdf, ps, dvi.
  1. Beata Madras. Basic Properties of Objects and Morphisms, Formalized Mathematics 6(3), pages 329-334, 1997. MML Identifier: ALTCAT_3
    Summary:
  2. Piotr Rudnicki, Andrzej Trybulec. Abian's Fixed Point Theorem, Formalized Mathematics 6(3), pages 335-338, 1997. MML Identifier: ABIAN
    Summary: A. Abian \cite{abi68} proved the following theorem: \begin{quotation} Let $f$ be a mapping from a finite set $D$. Then $f$ has a fixed point if and only if $D$ is not a union of three mutually disjoint sets $A$, $B$ and $C$ such that \[ A \cap f[A] = B \cap f[B] = C \cap f[C] = \emptyset.\] \end{quotation} (The range of $f$ is not necessarily the subset of its domain). The proof of the sufficiency is by induction on the number of elements of $D$. A.~M\c{a}kowski and K.~Wi{\'s}niewski \cite{maw69} have shown that the assumption of finiteness is superfluous. They proved their version of the theorem for $f$ being a function from $D$ into $D$. In the proof, the required partition was constructed and the construction used the axiom of choice. Their main point was to demonstrate that the use of this axiom in the proof is essential. We have proved in Mizar the generalized version of Abian's theorem, i.e. without assuming finiteness of $D$. We have simplified the proof from \cite{maw69} which uses well-ordering principle and transfinite ordinals---our proof does not use these notions but otherwise is based on their idea (we employ choice functions).
  3. Piotr Rudnicki, Andrzej Trybulec. On Same Equivalents of Well-foundedness, Formalized Mathematics 6(3), pages 339-343, 1997. MML Identifier: WELLFND1
    Summary: Four statements equivalent to well-foundedness (well-founded induction, existence of recursively defined functions, uniqueness of recursively defined functions, and absence of descending $\omega$-chains) have been proved in Mizar and the proofs were mechanically checked for correctness. It seems not to be widely known that the existence (without the uniqueness assumption) of recursively defined functions implies well-foundedness. In the proof we used regular cardinals, a fairly advanced notion of set theory. This work was inspired by T.~Franzen's paper ~\cite{tor96}. Franzen's proofs were written by a mathematician having an argument with a computer scientist. We were curious about the effort needed to formalize Franzen's proofs given the state of the Mizar Mathematical Library at that time (July 1996). The formalization went quite smoothly once the mathematics was sorted out.
  4. Robert Milewski. Algebraic and Arithmetic Lattices, Formalized Mathematics 6(3), pages 345-349, 1997. MML Identifier: WAYBEL13
    Summary: We formalize \cite[pp. 87--89]{CCL}.
  5. Yatsuka Nakamura, Roman Matuszewski, Adam Grabowski. Subsequences of Standard Special Circular Sequences in $\calE^2_\rmT$, Formalized Mathematics 6(3), pages 351-358, 1997. MML Identifier: JORDAN4
    Summary: It is known that a standard special circular sequence in ${\cal E}^2_{\rm T}$ properly defines a special polygon. We are interested in a part of such a sequence. It is shown that if the first point and the last point of the subsequence are different, it becomes a special polygonal sequence. The concept of ``a part of" is introduced, and the subsequence having this property can be characterized by using ``mid" function. For such subsequences, the concepts of ``Upper" and ``Lower" parts are introduced.
  6. Adam Grabowski. Lattice of Substitutions, Formalized Mathematics 6(3), pages 359-361, 1997. MML Identifier: SUBSTLAT
    Summary:
  7. Artur Kornilowicz. Equations in Many Sorted Algebras, Formalized Mathematics 6(3), pages 363-369, 1997. MML Identifier: EQUATION
    Summary: This paper is preparation to prove Birkhoff's Theorem. Some properties of many sorted algebras are proved. The last section of this work shows that every equation valid in a many sorted algebra is also valid in each subalgebra, and each image of it. Moreover for a family of many sorted algebras $(A_i: i \in I)$ if every equation is valid in each $A_i$, $i \in I$ then is also valid in product $\prod(A_i: i \in I)$.
  8. Robert Nieszczerzewski. Category of Functors Between Alternative Categories, Formalized Mathematics 6(3), pages 371-375, 1997. MML Identifier: FUNCTOR2
    Summary:
  9. Miroslaw Wojciechowski. Yoneda Embedding, Formalized Mathematics 6(3), pages 377-379, 1997. MML Identifier: YONEDA_1
    Summary:
  10. Christoph Schwarzweller. The Correctness of the Generic Algorithms of Brown and Henrici Concerning Addition and Multiplication in Fraction Fields, Formalized Mathematics 6(3), pages 381-388, 1997. MML Identifier: GCD_1
    Summary: We prove the correctness of the generic algorithms of Brown and Henrici concerning addition and multiplication in fraction fields of gcd-domains. For that we first prove some basic facts about divisibility in integral domains and introduce the concept of amplesets. After that we are able to define gcd-domains and to prove the theorems of Brown and Henrici which are crucial for the correctness of the algorithms. In the last section we define Mizar functions mirroring their input/output behaviour and prove properties of these functions that ensure the correctness of the algorithms.
  11. Artur Kornilowicz. Birkhoff Theorem for Many Sorted Algebras, Formalized Mathematics 6(3), pages 389-395, 1997. MML Identifier: BIRKHOFF
    Summary: \newcommand \pred[1]{${\cal P} #1$} In this article Birkhoff Variety Theorem for many sorted algebras is proved. A class of algebras is represented by predicate \pred{}. Notation \pred{[A]}, where $A$ is an algebra, means that $A$ is in class \pred{}. All algebras in our class are many sorted over many sorted signature $S$. The properties of varieties: \begin{itemize} \itemsep-3pt \item a class \pred{ } of algebras is abstract \item a class \pred{ } of algebras is closed under subalgebras \item a class \pred{ } of algebras is closed under congruences \item a class \pred{ } of algebras is closed under products \end{itemize} are published in this paper as: \begin{itemize} \itemsep-3pt \item for all non-empty algebras $A$, $B$ over $S$ such that $A$ and $B$ are\_isomorphic and \pred{[A]} holds \pred{[B]} \item for every non-empty algebra $A$ over $S$ and for strict non-empty subalgebra $B$ of $A$ such that \pred{[A]} holds \pred{[B]} \item for every non-empty algebra $A$ over $S$ and for every congruence $R$ of $A$ such that \pred{[A]} holds \pred{[A\slash R]} \item Let $I$ be a set and $F$ be an algebra family of $I$ over ${\cal A}.$ Suppose that for every set $i$ such that $i \in I$ there exists an algebra $A$ over ${\cal A}$ such that $A = F(i)$ and ${\cal P}[A]$. Then${\cal P}[\prod F]$. \end{itemize} This paper is formalization of parts of \cite{WECHLER}.
  12. Agnieszka Julia Marasik. Algebraic Operation on Subsets of Many Sorted Sets, Formalized Mathematics 6(3), pages 397-401, 1997. MML Identifier: CLOSURE3
    Summary:
  13. Yasunari Shidama, Artur Kornilowicz. Convergence and the Limit of Complex Sequences. Series, Formalized Mathematics 6(3), pages 403-410, 1997. MML Identifier: COMSEQ_3
    Summary:
  14. Jing-Chao Chen. The Steinitz Theorem and the Dimension of a Real Linear Space, Formalized Mathematics 6(3), pages 411-415, 1997. MML Identifier: RLVECT_5
    Summary: Finite-dimensional real linear spaces are defined. The dimension of such spaces is the cardinality of a basis. Obviously, each two basis have the same cardinality. We prove the Steinitz theorem and the Exchange Lemma. We also investigate some fundamental facts involving the dimension of real linear spaces.
  15. Yatsuka Nakamura, Piotr Rudnicki. Euler Circuits and Paths, Formalized Mathematics 6(3), pages 417-425, 1997. MML Identifier: GRAPH_3
    Summary: We prove the Euler theorem on existence of Euler circuits and paths in multigraphs.
  16. Czeslaw Bylinski, Piotr Rudnicki. Bounding Boxes for Compact Sets in $\calE^2$, Formalized Mathematics 6(3), pages 427-440, 1997. MML Identifier: PSCOMP_1
    Summary: We define pseudocompact topological spaces and prove that every compact space is pseudocompact. We also solve an exercise from \cite{mgm}~p.225 that for a topological space $X$ the following are equivalent: \begin{itemize} \item Every continuous real map from $X$ is bounded (i.e. $X$ is pseudocompact). \item Every continuous real map from $X$ attains minimum. \item Every continuous real map from $X$ attains maximum. \end{itemize} Finally, for a compact set in $E^2$ we define its bounding rectangle and introduce a collection of notions associated with the box.
  17. Czeslaw Bylinski, Piotr Rudnicki. The Scott Topology. Part II, Formalized Mathematics 6(3), pages 441-446, 1997. MML Identifier: WAYBEL14
    Summary: Mizar formalization of pp. 105--108 of \cite{CCL} which continues \cite{WAYBEL11.ABS}. We found a simplification for the proof of Corollary~1.15, in the last case, see the proof in the Mizar article for details.