VOLUME 3, NUMBER 2 (1992), Formalized Mathematics, ISSN 0777-4028

Formalized Mathematics (ISSN 0777-4028)
Volume 3, Number 2 (1992): pdf, ps, dvi.

Yatsuka Nakamura, Jaroslaw Kotowicz. The Jordan's Property for Certain Subsets of the Plane, Formalized Mathematics 3(2), pages 137-142, 1992. MML Identifier: JORDAN1
Summary: Let $S$ be a subset of the topological Euclidean plane ${\cal E}^2_{\rm T}$. We say that $S$ has Jordan's property if there exist two non-empty, disjoint and connected subsets $G_1$ and $G_2$ of ${\cal E}^2_{\rm T}$ such that $S \mathclose{^{\rm c}} = G_1 \cup G_2$ and $\overline{G_1} \setminus G_1 = \overline{G_2} \setminus{G_2}$ (see \cite{TAKE-NAKA}, \cite{Dick}). The aim is to prove that the boundaries of some special polygons in ${\cal E}^2_{\rm T}$ have this property (see Section 3). Moreover, it is proved that both the interior and the exterior of the boundary of any rectangle in ${\cal E}^2_{\rm T}$ is open and connected.
Zbigniew Karno. The Lattice of Domains of an Extremally Disconnected Space, Formalized Mathematics 3(2), pages 143-149, 1992. MML Identifier: TDLAT_3
Summary: Let $X$ be a topological space and let $A$ be a subset of $X$. Recall that $A$ is said to be a {\em domain}\/ in $X$ provided ${\rm Int}\, \overline{A} \subseteq A \subseteq \overline{{\rm Int}\,A}$ (see \cite{TOPS_1.ABS}, \cite{ISOMICHI}). Recall also that $A$ is said to be a(n) {\em closed}\/ ({\em open})\/ {\em domain}\/ in $X$ if $A = \overline{{\rm Int}\,A}$ ($A = {\rm Int}\,\overline{A}$, resp.) (see e.g. \cite{KURAT:2}, \cite{TOPS_1.ABS}). It is well-known that for a given topological space all its closed domains form a Boolean lattice, and similarly all its open domains form a Boolean lattice, too (see e.g., \cite{MOST-KURAT:3}, \cite{BIRKHOFF:1}). In \cite{TDLAT_1.ABS} it is proved that all domains of a given topological space form a complemented lattice. One may ask whether the lattice of all domains is Boolean. The aim is to give an answer to this question.\par To present the main results we first recall the definition of a class of topological spaces which is important here. $X$ is called {\em extremally disconnected}\/ if for every open subset $A$ of $X$ the closure $\overline {A}$ is open in $X$ \cite{STONE:1} (comp. \cite{ENGEL:1}). It is shown here, using Mizar System, that {\em the lattice of all domains of a topological space $X$ is modular iff $X$ is extremally disconnected.} Moreover, for every extremally disconnected space the lattice of all its domains coincides with both the lattice of all its closed domains and the lattice of all its open domains. From these facts it follows that {\em the lattice of all domains of a topological space $X$ is Boolean iff $X$ is extremally disconnected.}\par Note that we also review some of the standard facts on discrete, anti-discrete, almost discrete, extremally disconnected and hereditarily extremally disconnected topological spaces (comp. \cite{KURAT:2}, \cite{ENGEL:1}).
Yatsuka Nakamura, Andrzej Trybulec. A Mathematical Model of CPU, Formalized Mathematics 3(2), pages 151-160, 1992. MML Identifier: AMI_1
Summary: This paper is based on a previous work of the first author \cite{NAKAMURA1} in which a mathematical model of the computer has been presented. The model deals with random access memory, such as RASP of C. C. Elgot and A. Robinson \cite{ELGOT-ROBIN}, however, it allows for a more realistic modeling of real computers. This new model of computers has been named by the author (Y. Nakamura, \cite{NAKAMURA1}) Architecture Model for Instructions (AMI). It is more developed than previous models, both in the description of hardware (e.g., the concept of the program counter, the structure of memory) as well as in the description of instructions (instruction codes, addresses). The structure of AMI over an arbitrary collection of mathematical domains N consists of: \begin{description} \item{ - }a non-empty set of objects, \item{ - }the instruction counter, \item{ - }a non-empty set of objects called instruction locations, \item{ - }a non-empty set of instruction codes, \item{ - }an instruction code for halting, \item{ - }a set of instructions that are ordered pairs with the first element being an instruction code and the second a finite sequence in which members are either objects of the AMI or elements of one of the domains included in N, \item{ - }a function that assigns to every object of AMI its kind that is either {\em an instruction} or {\em an instruction location} or an element of N, \item{ - }a function that assigns to every instruction its execution that is again a function mapping states of AMI into the set of states. \end{description} By a state of AMI we mean a function that assigns to every object of AMI an element of the same kind. In this paper we develop the theory of AMI. Some properties of AMI are introduced ensuring it to have some properties of real computers: \begin{description} \item{ - }a von Neumann AMI, in which only addresses to instruction locations are stored in the program counter, \item{ - }data oriented, those in which instructions cannot be stored in data locations, \item{ - }halting, in which the execution of the halt instruction is the identity mapping of the states of an AMI, \item{ - }steady programmed, the condition in which the contents of the instruction locations do not change during execution, \item{ - }definite, a property in which only instructions may be stored in instruction locations. \end{description} We present an example of AMI called a Small Concrete Model which has been constructed in \cite{NAKAMURA1}. The Small Concrete Model has only one kind of data: integers and a set of instructions, small but sufficient to cope with integers.
Czeslaw Bylinski. Cartesian Categories, Formalized Mathematics 3(2), pages 161-169, 1992. MML Identifier: CAT_4
Summary: We define and prove some simple facts on Cartesian categories and its duals co-Cartesian categories. The Cartesian category is defined as a category with the fixed terminal object, the fixed projections, and the binary products. Category $C$ has finite products if and only if $C$ has a terminal object and for every pair $a, b$ of objects of $C$ the product $a\times b$ exists. We say that a category $C$ has a finite product if every finite family of objects of $C$ has a product. Our work is based on ideas of \cite{SZABO}, where the algebraic properties of the proof theory are investigated. The terminal object of a Cartesian category $C$ is denoted by $\hbox{\bf 1}_C$. The binary product of $a$ and $b$ is written as $a\times b$. The projections of the product are written as $pr_1(a,b)$ and as $pr_2(a,b)$. We define the products $f\times g$ of arrows $f: a\rightarrow a'$ and $g: b\rightarrow b'$ as $:a\times b\rightarrow a'\times b'$.\par Co-Cartesian category is defined dually to the Cartesian category. Dual to a terminal object is an initial object, and to products are coproducts. The initial object of a Cartesian category $C$ is written as $\hbox{\bf 0}_C$. Binary coproduct of $a$ and $b$ is written as $a+b$. Injections of the coproduct are written as $in_1(a,b)$ and as $in_2(a,b)$.
Hiroshi Yamazaki, Yasunari Shidama. Algebra of Vector Functions, Formalized Mathematics 3(2), pages 171-175, 1992. MML Identifier: VFUNCT_1
Summary: We develop the algebra of partial vector functions, with domains being algebra of vector functions.
Zbigniew Karno. On a Duality between Weakly Separated Subspaces of Topological Spaces, Formalized Mathematics 3(2), pages 177-182, 1992. MML Identifier: TSEP_2
Summary: Let $X$ be a topological space and let $X_{1}$ and $X_{2}$ be subspaces of $X$ with the carriers $A_{1}$ and $A_{2}$, respectively. Recall that $X_{1}$ and $X_{2}$ are {\em weakly separated}\/ if $A_{1} \setminus A_{2}$ and $A_{2} \setminus A_{1}$ are separated (see \cite{TSEP_1.ABS} and also \cite{TMAP_1.ABS} for applications). Our purpose is to list a number of properties of such subspaces, supplementary to those given in \cite{TSEP_1.ABS}. Note that in the Mizar formalism the carrier of any topological space (hence the carrier of any its subspace) is always non--empty, therefore for convenience we list beforehand analogous properties of weakly separated subsets without any additional conditions.\par To present the main results we first formulate a useful definition. We say that $X_{1}$ and $X_{2}$ {\em constitute a decomposition}\/ of $X$ if $A_{1}$ and $A_{2}$ are disjoint and the union of $A_{1}$ and $A_{2}$ covers the carrier of $X$ (comp. \cite{KURAT:2}). We are ready now to present the following duality property between pairs of weakly separated subspaces~: {\em If each pair of subspaces $X_{1}$, $Y_{1}$ and $X_{2}$, $Y_{2}$ of $X$ constitutes a decomposition of $X$, then $X_{1}$ and $X_{2}$ are weakly separated iff $Y_{1}$ and $Y_{2}$ are weakly separated}. From this theorem we get immediately that under the same hypothesis, {\em $X_{1}$ and $X_{2}$ are separated iff $X_{1}$ misses $X_{2}$ and $Y_{1}$ and $Y_{2}$ are weakly separated}. Moreover, we show the following enlargement theorem~: {\em If $X_{i}$ and $Y_{i}$ are subspaces of $X$ such that $Y_{i}$ is a subspace of $X_{i}$ and $Y_{1} \cup Y_{2} = X_{1} \cup X_{2}$ and if $Y_{1}$ and $Y_{2}$ are weakly separated, then $X_{1}$ and $X_{2}$ are weakly separated}. We show also the following dual extenuation theorem~: {\em If $X_{i}$ and $Y_{i}$ are subspaces of $X$ such that $Y_{i}$ is a subspace of $X_{i}$ and $Y_{1} \cap Y_{2} = X_{1} \cap X_{2}$ and if $X_{1}$ and $X_{2}$ are weakly separated, then $Y_{1}$ and $Y_{2}$ are weakly separated}. At the end we give a few properties of weakly separated subspaces in subspaces.
Pauline N. Kawamoto, Yasushi Fuwa, Yatsuka Nakamura. Basic Petri Net Concepts, Formalized Mathematics 3(2), pages 183-187, 1992. MML Identifier: PETRI
Summary: This article presents the basic place/transition net structure definition for building various types of Petri nets. The basic net structure fields include places, transitions, and arcs (place-transition, transition-place) which may be supplemented with other fields (e.g., capacity, weight, marking, etc.) as needed. The theorems included in this article are divided into the following categories: deadlocks, traps, and dual net theorems. Here, a dual net is taken as the result of inverting all arcs (place-transition arcs to transition-place arcs and vice-versa) in the original net.
Hiroshi Imura, Masayoshi Eguchi. Finite Topological Spaces, Formalized Mathematics 3(2), pages 189-193, 1992. MML Identifier: FIN_TOPO
Summary: By borrowing the concept of neighbourhood from the theory of topological space in continuous cases and extending it to a discrete case such as a space of lattice points we have defined such concepts as boundaries, closures, interiors, isolated points, and connected points as in the case of continuity. We have proved various properties which are satisfied by these concepts.
Grzegorz Bancerek. Sets and Functions of Trees and Joining Operations of Trees, Formalized Mathematics 3(2), pages 195-204, 1992. MML Identifier: TREES_3
Summary: In the article we deal with sets of trees and functions yielding trees. So, we introduce the sets of all trees, all finite trees and of all trees decorated by elements from some set. Next, the functions and the finite sequences yielding (finite, decorated) trees are introduced. There are shown some convenient but technical lemmas and clusters concerning with those concepts. In the fourth section we deal with trees decorated by Cartesian product and we introduce the concept of a tree called a substitution of structure of some finite tree. Finally, we introduce the operations of joining trees, i.e. for the finite sequence of trees we define the tree which is made by joining the trees from the sequence by common root. For one and two trees there are introduced the same operations.
Katarzyna Zawadzka. The Sum and Product of Finite Sequences of Elements of a Field, Formalized Mathematics 3(2), pages 205-211, 1992. MML Identifier: FVSUM_1
Summary: This article is concerned with a generalization of concepts introduced in \cite{RVSUM_1.ABS}, i.e., there are introduced the sum and the product of finite number of elements of any field. Moreover, the product of vectors which yields a vector is introduced. According to \cite{RVSUM_1.ABS}, some operations on $i$-tuples of elements of field are introduced: addition, subtraction, and complement. Some properties of the sum and the product of finite number of elements of a field are present.
Grzegorz Bancerek. Monoids, Formalized Mathematics 3(2), pages 213-225, 1992. MML Identifier: MONOID_0
Summary: The goal of the article is to define the concept of monoid. In the preliminary section we introduce the notion of some properties of binary operations. The second section is concerning with structures with a set and a binary operation on this set: there is introduced the notion corresponding to the notion of some properties of binary operations and there are shown some useful clusters. Next, we are concerning with the structure with a set, a binary operation on the set and with an element of the set. Such a structure is called monoid iff the operation is associative and the element is a unity of the operation. In the fourth section the concept of subsystems of monoid (group) is introduced. Subsystems are submonoids (subgroups) or other parts of monoid (group) with are closed w.r.t. the operation. There are presented facts on inheritness of some properties by subsystems. Finally, there are constructed the examples of groups and monoids: the group $\rangle{\Bbb R},+\langle$ of real numbers with addition, the group ${\Bbb Z}^+$ of integers as the subsystem of the group $\rangle{\Bbb R},+\langle$, the semigroup $\rangle{\Bbb N},+\langle$ of natural numbers as the subsystem of ${\Bbb Z}^+$, and the monoid $\rangle{\Bbb N},+,0\langle$ of natural numbers with addition and zero as monoidal extension of the semigroup $\rangle{\Bbb N},+\langle$. The semigroups of real and natural numbers with multiplication are also introduced. The monoid of finite sequences over some set with concatenation as binary operation and with empty sequence as neutral element is defined in sixth section. Last section deals with monoids with the composition of functions as the operation, i.e. with the monoid of partial and total functions and the monoid of permutations.
Grzegorz Bancerek. Monoid of Multisets and Subsets, Formalized Mathematics 3(2), pages 227-233, 1992. MML Identifier: MONOID_1
Summary: The monoid of functions yielding elements of a group is introduced. The monoid of multisets over a set is constructed as such monoid where the target group is the group of natural numbers with addition. Moreover, the generalization of group operation onto the operation on subsets is present. That generalization is used to introduce the group $2^G$ of subsets of a group $G$.
Anna Lango, Grzegorz Bancerek. Product of Families of Groups and Vector Spaces, Formalized Mathematics 3(2), pages 235-240, 1992. MML Identifier: PRVECT_1
Summary: In the first section we present properties of fields and Abelian groups in terms of commutativity, associativity, etc. Next, we are concerned with operations on $n$-tuples on some set which are generalization of operations on this set. It is used in third section to introduce the $n$-power of a group and the $n$-power of a field. Besides, we introduce a concept of indexed family of binary (unary) operations over some indexed family of sets and a product of such families which is binary (unary) operation on a product of family sets. We use that product in the last section to introduce the product of a finite sequence of Abelian groups.
Yatsuka Nakamura, Andrzej Trybulec. On a Mathematical Model of Programs, Formalized Mathematics 3(2), pages 241-250, 1992. MML Identifier: AMI_2
Summary: We continue the work on mathematical modeling of hardware and software started in \cite{AMI_1.ABS}. The main objective of this paper is the definition of a program. We start with the concept of partial product, i.e. the set of all partial functions $f$ from $I$ to $\bigcup_{i\in I} A_i$, fulfilling the condition $f.i \in A_i$ for $i \in dom f$. The computation and the result of a computation are defined in usual way. A finite partial state is called autonomic if the result of a computation starting with it does not depend on the remaining memory and an AMI is called programmable if it has a non empty autonomic partial finite state. We prove the consistency of the following set of properties of an AMI: data-oriented, halting, steady-programmed, realistic and programmable. For this purpose we define a trivial AMI. It has only the instruction counter and one instruction location. The only instruction of it is the halt instruction. A preprogram is a finite partial state that halts. We conclude with the definition of a program of a partial function $F$ mapping the set of the finite partial states into itself. It is a finite partial state $s$ such that for every finite partial state $s' \in dom F$ the result of any computation starting with $s+s'$ includes $F.s'$.
Jaroslaw Kotowicz, Beata Madras, Malgorzata Korolkiewicz. Basic Notation of Universal Algebra, Formalized Mathematics 3(2), pages 251-253, 1992. MML Identifier: UNIALG_1
Summary: We present the basic notation of universal algebra.
Jaroslaw Kotowicz, Konrad Raczkowski. Coherent Space, Formalized Mathematics 3(2), pages 255-261, 1992. MML Identifier: COH_SP
Summary: Coherent Space, web of coherent space and two categories: category of coherent spaces and category of tolerances on same fixed set.
Jozef Bialas. Properties of the Intervals of Real Numbers, Formalized Mathematics 3(2), pages 263-269, 1992. MML Identifier: MEASURE5
Summary: The paper contains definitions and basic properties of the intervals of real numbers.\par The article includes the text being a continuation of the paper \cite{MEASURE4.ABS}. Some theorems concerning basic properties of intervals are proved.
Wojciech A. Trybulec. Subspaces of Real Linear Space generated by One, Two, or Three Vectors and Their Cosets, Formalized Mathematics 3(2), pages 271-274, 1992. MML Identifier: RLVECT_4
Summary:
Jaroslaw Kotowicz. Functions and Finite Sequences of Real Numbers, Formalized Mathematics 3(2), pages 275-278, 1992. MML Identifier: RFINSEQ
Summary: We define notions of fiberwise equipotent functions, non-increasing finite sequences of real numbers and new operations on finite sequences. Equivalent conditions for fiberwise equivalent functions and basic facts about new constructions are shown.
Jaroslaw Kotowicz, Yuji Sakai. Properties of Partial Functions from a Domain to the Set of Real Numbers, Formalized Mathematics 3(2), pages 279-288, 1992. MML Identifier: RFUNCT_3
Summary: The article consists of two parts. In the first one we consider notion of nonnegative and nonpositive part of a real numbers. In the second we consider partial function from a domain to the set of real numbers (or more general to a domain). We define a few new operations for these functions and show connections between finite sequences of real numbers and functions which domain is finite. We introduce {\em integrations} for finite domain real valued functions.
Michal Muzalewski. Domains of Submodules, Join and Meet of Finite Sequences of Submodules and Quotient Modules, Formalized Mathematics 3(2), pages 289-296, 1992. MML Identifier: LMOD_7
Summary: Notions of domains of submodules, join and meet of finite sequences of submodules and quotient modules. A few basic theorems and schemes related to these notions are proved.
Zbigniew Karno. Remarks on Special Subsets of Topological Spaces, Formalized Mathematics 3(2), pages 297-303, 1992. MML Identifier: TOPS_3
Summary: Let $X$ be a topological space and let $A$ be a subset of $X$. Recall that $A$ is {\em nowhere dense}\/ in $X$ if its closure is a boundary subset of $X$, i.e., if ${\rm Int}\,\overline{A} = \emptyset$ (see \cite{KURAT:2}). We introduce here the concept of everywhere dense subsets in $X$, which is dual to the above one. Namely, $A$ is said to be {\em everywhere dense}\/ in $X$ if its interior is a dense subset of $X$, i.e., if $\overline{{\rm Int}\,A} =$ the carrier of $X$.\par Our purpose is to list a number of properties of such sets (comp. \cite{TOPS_1.ABS}). As a sample we formulate their two dual characterizations. The first one characterizes thin sets in $X$~: {\em $A$ is nowhere dense iff for every open nonempty subset $G$ of $X$ there is an open nonempty subset of $X$ contained in $G$ and disjoint from $A$}. The corresponding second one characterizes thick sets in $X$~: {\em $A$ is everywhere dense iff for every closed subset $F$ of $X$ distinct from the carrier of $X$ there is a closed subset of $X$ distinct from the carrier of $X$, which contains $F$ and together with $A$ covers the carrier of $X$}. We also give some connections between both these concepts. Of course, {\em $A$ is everywhere (nowhere) dense in $X$ iff its complement is nowhere (everywhere) dense}. Moreover, {\em $A$ is nowhere dense iff there are two subsets of $X$, $C$ boundary closed and $B$ everywhere dense, such that $A = C \cap B$ and $C \cup B$ covers the carrier of $X$}. Dually, {\em $A$ is everywhere dense iff there are two disjoint subsets of $X$, $C$ open dense and $B$ nowhere dense, such that $A = C \cup B$}.\par Note that some relationships between everywhere (nowhere) dense sets in $X$ and everywhere (nowhere) dense sets in subspaces of $X$ are also indicated.
Zbigniew Karno. On Discrete and Almost Discrete Topological Spaces, Formalized Mathematics 3(2), pages 305-310, 1992. MML Identifier: TEX_1
Summary: A topological space $X$ is called {\em almost discrete}\/ if every open subset of $X$ is closed; equivalently, if every closed subset of $X$ is open (comp. \cite{KURAT:2},\cite{KURAT:3}). Almost discrete spaces were investigated in Mizar formalism in \cite{TDLAT_3.ABS}. We present here a few properties of such spaces supplementary to those given in \cite{TDLAT_3.ABS}.\par Most interesting is the following characterization~: {\em A topological space $X$ is almost discrete iff every nonempty subset of $X$ is not nowhere dense}. Hence, {\em $X$ is non almost discrete iff there is an everywhere dense subset of $X$ different from the carrier of $X$}. We have an analogous characterization of discrete spaces~: {\em A topological space $X$ is discrete iff every nonempty subset of $X$ is not boundary}. Hence, {\em $X$ is non discrete iff there is a dense subset of $X$ different from the carrier of $X$}. It is well known that the class of all almost discrete spaces contains both the class of discrete spaces and the class of anti-discrete spaces (see e.g., \cite{TDLAT_3.ABS}). Observations presented here show that the class of all almost discrete non discrete spaces is not contained in the class of anti-discrete spaces and the class of all almost discrete non anti-discrete spaces is not contained in the class of discrete spaces. Moreover, the class of almost discrete non discrete non anti-discrete spaces is nonempty. To analyse these interdependencies we use various examples of topological spaces constructed here in Mizar formalism.