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

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

Zbigniew Karno. Continuity of Mappings over the Union of Subspaces, Formalized Mathematics 3(1), pages 1-16, 1992. MML Identifier: TMAP_1
Summary: Let $X$ and $Y$ be topological spaces and let $X_{1}$ and $X_{2}$ be subspaces of $X$. Let $f : X_{1} \cup X_{2} \rightarrow Y$ be a mapping defined on the union of $X_{1}$ and $X_{2}$ such that the restriction mappings $f_{\mid X_{1}}$ and $f_{\mid X_{2}}$ are continuous. It is well known that if $X_{1}$ and $X_{2}$ are both open (closed) subspaces of $X$, then $f$ is continuous (see e.g. \cite[p.106]{KURAT:2}). \par The aim is to show, using Mizar System, the following theorem (see Section 5): {\em If $X_{1}$ and $X_{2}$ are weakly separated, then $f$ is continuous} (compare also \cite[p.358]{CECH:1} for related results). This theorem generalizes the preceding one because if $X_{1}$ and $X_{2}$ are both open (closed), then these subspaces are weakly separated (see \cite{TSEP_1.ABS}). However, the following problem remains open. \begin{itemize} \item[ ] {\bf Problem 1.} Characterize the class of pairs of subspaces $X_{1}$ and $X_{2}$ of a topological space $X$ such that ($\ast$) for any topological space $Y$ and for any mapping $f : X_{1} \cup X_{2} \rightarrow Y$, $f$ is continuous if the restrictions $f_{\mid X_{1}}$ and $f_{\mid X_{2}}$ are continuous. \end{itemize} In some special case we have the following characterization: {\em $X_{1}$ and $X_{2}$ are separated iff $X_{1}$ misses $X_{2}$ and the condition} ($\ast$) {\em is fulfilled.} In connection with this fact we hope that the following specification of the preceding problem has an affirmative answer. \begin{itemize} \item[ ] {\bf Problem 2.} Suppose the condition ($\ast$) is fulfilled. Must $X_{1}$ and $X_{2}$ be weakly separated ? \end{itemize} Note that in the last section the concept of the union of two mappings is introduced and studied. In particular, all results presented above are reformulated using this notion. In the remaining sections we introduce concepts needed for the formulation and the proof of theorems on properties of continuous mappings, restriction mappings and modifications of the topology.
Beata Perkowska. Functional Sequence from a Domain to a Domain, Formalized Mathematics 3(1), pages 17-21, 1992. MML Identifier: SEQFUNC
Summary: Definitions of functional sequences and basic operations on functional sequences from a domain to a domain, point and uniform convergence, limit of functional sequence from a domain to the set of real numbers and facts about properties of the limit of functional sequences are proved.
Michal Muzalewski. Reper Algebras, Formalized Mathematics 3(1), pages 23-28, 1992. MML Identifier: MIDSP_3
Summary: We shall describe $n$-dimensional spaces with the reper operation \cite[pages 72--79]{MUZALEWSKI:1}. An inspiration to such approach comes from the monograph \cite{SZMIELEW:1} and so-called Leibniz program. Let us recall that the Leibniz program is a program of algebraization of geometry using purely geometric notions. Leibniz formulated his program in opposition to algebraization method developed by Descartes. The Euclidean geometry in Szmielew's approach \cite {SZMIELEW:1} is a theory of structures $\langle S$; $\parallel, \oplus, O \rangle$, where $\langle S$; $\parallel, \oplus, O \rangle$ is Desarguesian midpoint plane and $O \subseteq S\times S\times S$ is the relation of equi-orthogonal basis. Points $o, p, q$ are in relation $O$ if they form an isosceles triangle with the right angle in vertex $a$. If we fix vertices $a, p$, then there exist exactly two points $q, q'$ such that $O(apq)$, $O(apq')$. Moreover $q \oplus q' = a$. In accordance with the Leibniz program we replace the relation of equi-orthogonal basis by a binary operation $\ast : S\times S \rightarrow S$, called the reper operation. A standard model for the Euclidean geometry in the above sense is the oriented plane over the field of real numbers with the reper operations $\ast$ defined by the condition: $a \ast b = q$ iff the point $q$ is the result of rotating of $p$ about right angle around the center $a$.
Dariusz Surowik. Isomorphisms of Cyclic Groups. Some Properties of Cyclic Groups, Formalized Mathematics 3(1), pages 29-32, 1992. MML Identifier: GR_CY_2
Summary: Some theorems and properties of cyclic groups have been proved with special regard to isomorphisms of these groups. Among other things it has been proved that an arbitrary cyclic group is isomorphic with groups of integers with addition or group of integers with addition modulo $m$. Moreover, it has been proved that two arbitrary cyclic groups of the same order are isomorphic and that the class of cyclic groups is closed in consideration of homomorphism images. Some other properties of groups of this type have been proved too.
Andrzej Trybulec. Some Isomorphisms Between Functor Categories, Formalized Mathematics 3(1), pages 33-40, 1992. MML Identifier: ISOCAT_2
Summary: We define some well known isomorphisms between functor categories: between $A^{\mathop{\dot\circlearrowright}(o,m)}$ and $A$, between $C^{\mizleftcart A,B\mizrightcart}$ and ${(C^B)}^A$, and between ${\mizleftcart B,C\mizrightcart}^A$ and $\mizleftcart B^A,C^A\mizrightcart$. Compare \cite{SEMAD} and \cite{MacLane:1}. Unfortunately in this paper "functor" is used in two different meanings, as a lingual function and as a functor between categories.
Toshihiko Watanabe. The Lattice of Domains of a Topological Space, Formalized Mathematics 3(1), pages 41-46, 1992. MML Identifier: TDLAT_1
Summary: Let $T$ be a topological space and let $A$ be a subset of $T$. Recall that $A$ is said to be a {\em closed domain} of $T$ if $A = \overline{{\rm Int}\,A}$ and $A$ is said to be an {\em open domain} of $T$ if $A = {\rm Int}\,\overline{A}$ (see e.g. \cite{KURAT:2}, \cite{TOPS_1.ABS}). Some simple generalization of these notions is the following one. $A$ is said to be a {\em domain} of $T$ provided ${\rm Int}\,\overline{A} \subseteq A \subseteq \overline{{\rm Int}\,A}$ (see \cite{TOPS_1.ABS} and compare \cite{ISOMICHI}). In this paper certain connections between these concepts are introduced and studied. \par Our main results are concerned with the following well--known theorems (see e.g. \cite{MOST-KURAT:3}, \cite{BIRKHOFF:1}). For a given topological space all its closed domains form a Boolean lattice, and similarly all its open domains form a Boolean lattice, too. It is proved that {\em all domains of a given topological space form a complemented lattice.} Moreover, it is shown that both {\em the lattice of open domains and the lattice of closed domains are sublattices of the lattice of all domains.} In the beginning some useful theorems about subsets of topological spaces are proved and certain properties of domains, closed domains and open domains are discussed.
Michal Muzalewski. Submodules, Formalized Mathematics 3(1), pages 47-51, 1992. MML Identifier: LMOD_6
Summary: This article contains the notions of trivial and non-trivial leftmodules and rings, cyclic submodules and inclusion of submodules. A few basic theorems related to these notions are proved.
Jaroslaw Zajkowski. Oriented Metric-Affine Plane -- Part II, Formalized Mathematics 3(1), pages 53-56, 1992. MML Identifier: DIRORT
Summary: Axiomatic description of properties of the oriented orthogonality relation. Next we construct (with the help of the oriented orthogonality relation) vector space and give the definitions of left-, right-, and semi-transitives.
Michal Muzalewski. Opposite Rings, Modules and their Morphisms, Formalized Mathematics 3(1), pages 57-65, 1992. MML Identifier: MOD_4
Summary: Let $\Bbb K = \langle S; K, 0, 1, +, \cdot \rangle$ be a ring. The structure ${}^{\rm op}\Bbb K = \langle S; K, 0, 1, +, \bullet \rangle$ is called anti-ring, if $\alpha \bullet \beta = \beta \cdot \alpha$ for elements $\alpha$, $\beta$ of $K$ \cite[pages 5--7]{MUZALEWSKI:1}. It is easily seen that ${}^{\rm op}\Bbb K$ is also a ring. If $V$ is a left module over $\Bbb K$, then $V$ is a right module over ${}^{\rm op}\Bbb K$. If $W$ is a right module over $\Bbb K$, then $W$ is a left module over ${}^{\rm op}\Bbb K$. Let $K, L$ be rings. A morphism $J: K \longrightarrow L$ is called anti-homomorphism, if $J(\alpha\cdot\beta) = J(\beta)\cdot J(\alpha)$ for elements $\alpha$, $\beta$ of $K$. If $J:K \longrightarrow L$ is a homomorphism, then $J:K \longrightarrow {}^{\rm op}L$ is an anti-homomorphism. Let $K, L$ be rings, $V, W$ left modules over $K, L$ respectively and $J:K \longrightarrow L$ an anti-monomorphism. A map $f:V \longrightarrow W$ is called $J$ - semilinear, if $f(x+y) = f(x)+f(y)$ and $f(\alpha\cdot x) = J(\alpha)\cdot f(x)$ for vectors $x, y$ of $V$ and a scalar $\alpha$ of $K$.
Jozef Bialas. Properties of Caratheodor's Measure, Formalized Mathematics 3(1), pages 67-70, 1992. MML Identifier: MEASURE4
Summary: The paper contains definitions and basic properties of Ca\-ra\-the\-o\-dory measure, with values in $\overline{\Bbb R}$, the enlarged set of real numbers, where $\overline{\Bbb R}$ denotes set $\overline{\Bbb R} = {\Bbb R}\cup\{-\infty,+\infty\}$ - by \cite{SIKORSKI:1}. The article includes the text being a continuation of the paper \cite{MEASURE3.ABS}. Caratheodory theorem and some theorems concerning basic properties of Caratheodory measure are proved. The work is the sixth part of the series of articles concerning the Lebesgue measure theory.
Zbigniew Karno, Toshihiko Watanabe. Completeness of the Lattices of Domains of a Topological Space, Formalized Mathematics 3(1), pages 71-79, 1992. MML Identifier: TDLAT_2
Summary: Let $T$ be a topological space and let $A$ be a subset of $T$. Recall that $A$ is said to be a {\em domain} in $T$ provided ${\rm Int}\,\overline{A} \subseteq A \subseteq \overline{{\rm Int}\,A}$ (see \cite{TOPS_1.ABS} and comp. \cite{ISOMICHI}). This notion is a simple generalization of the notions of open and closed domains in $T$ (see \cite{TOPS_1.ABS}). Our main result is concerned with an extension of the following well--known theorem (see e.g. \cite{BIRKHOFF:1}, \cite{MOST-KURAT:3}, \cite{ENGEL:1}). For a given topological space the Boolean lattices of all its closed domains and all its open domains are complete. It is proved here, using Mizar System, that {\em the complemented lattice of all domains of a given topological space is complete}, too (comp. \cite{TDLAT_1.ABS}).\par It is known that both the lattice of open domains and the lattice of closed domains are sublattices of the lattice of all domains \cite{TDLAT_1.ABS}. However, the following two problems remain open. \begin{itemize} \item[ ] {\bf Problem 1.} Let $L$ be a sublattice of the lattice of all domains. Suppose $L$ is complete, is smallest with respect to inclusion, and contains as sublattices the lattice of all closed domains and the lattice of all open domains. Must $L$ be equal to the lattice of all domains~? \end{itemize} A domain in $T$ is said to be a {\em Borel domain} provided it is a Borel set. Of course every open (closed) domain is a Borel domain. It can be proved that all Borel domains form a sublattice of the lattice of domains. \begin{itemize} \item[ ] {\bf Problem 2.} Let $L$ be a sublattice of the lattice of all domains. Suppose $L$ is smallest with respect to inclusion and contains as sublattices the lattice of all closed domains and the lattice of all open domains. Must $L$ be equal to the lattice of all Borel domains~? \end{itemize} Note that in the beginning the closure and the interior operations for families of subsets of topological spaces are introduced and their important properties are presented (comp. \cite{KURAT:2}, \cite{KURAT:4}, \cite{MOST-KURAT:3}). Using these notions, certain properties of domains, closed domains and open domains are studied (comp. \cite{KURAT:4}, \cite{ENGEL:1}).
Leszek Borys. On Paracompactness of Metrizable Spaces, Formalized Mathematics 3(1), pages 81-84, 1992. MML Identifier: PCOMPS_2
Summary: The aim is to prove, using Mizar System, one of the most important result in general topology, namely the Stone Theorem on paracompactness of metrizable spaces \cite{STONE:2}. Our proof is based on \cite{RUDIN:1} (and also \cite{PATKOWSKA:74}). We prove first auxiliary fact that every open cover of any metrizable space has a locally finite open refinement. We show next the main theorem that every metrizable space is paracompact. The remaining material is devoted to concepts and certain properties needed for the formulation and the proof of that theorem (see also \cite{PCOMPS_1.ABS}).
Toshihiko Watanabe. The Brouwer Fixed Point Theorem for Intervals, Formalized Mathematics 3(1), pages 85-88, 1992. MML Identifier: TREAL_1
Summary: The aim is to prove, using Mizar System, the following simplest version of the Brouwer Fixed Point Theorem \cite{BROUWER:1}. {\em For every continuous mapping $f : {\Bbb I} \rightarrow {\Bbb I}$ of the topological unit interval $\Bbb I$ there exists a point $x$ such that $f(x) = x$} (see e.g. \cite{DUG-GRAN:1}, \cite{BROWN:1}).
Grzegorz Bancerek. On Powers of Cardinals, Formalized Mathematics 3(1), pages 89-93, 1992. MML Identifier: CARD_5
Summary: In the first section the results of \cite[axiom (30)]{AXIOMS.ABS}\footnote {Axiom (30)\quad ---\quad $n = \{k\in{\Bbb N}: k < n\}$ for every natural number $n$.}, i.e. the correspondence between natural and ordinal (cardinal) numbers are shown. The next section is concerned with the concepts of infinity and cofinality (see \cite{ZFREFLE1.ABS}), and introduces alephs as infinite cardinal numbers. The arithmetics of alephs, i.e. some facts about addition and multiplication, is present in the third section. The concepts of regular and irregular alephs are introduced in the fourth section, and the fact that $\aleph_0$ and every non-limit cardinal number are regular is proved there. Finally, for every alephs $\alpha$ and $\beta$ $$\alpha^\beta = \left\{ \begin{array}{ll} 2^\beta,& {\rm if}\ \alpha\leq\beta,\\ \sum_{\gamma<\alpha}\gamma^\beta,& {\rm if}\ \beta < {\rm cf}\alpha\ {\rm and} \ \alpha\ {\rm is\ limit\ cardinal},\\ \left(\sum_{\gamma<\alpha}\gamma^\beta\right)^{\rm cf\alpha},& {\rm if\ cf}\alpha \leq \beta \leq \alpha.\\ \end{array}\right.$$ \\ Some proofs are based on \cite{GUZ-ZBIER:1}.
Yatsuka Nakamura, Jaroslaw Kotowicz. Basic Properties of Connecting Points with Line Segments in $\calE^2_\rmT$, Formalized Mathematics 3(1), pages 95-99, 1992. MML Identifier: TOPREAL3
Summary: Some properties of line segments in 2-dimensional Euclidean space and some relations between line segments and balls are proved.
Yatsuka Nakamura, Jaroslaw Kotowicz. Connectedness Conditions Using Polygonal Arcs, Formalized Mathematics 3(1), pages 101-106, 1992. MML Identifier: TOPREAL4
Summary: A concept of special polygonal arc joining two different points is defined. Any two points in a ball can be connected by this kind of arc, and that is also true for any region in ${\cal E}^2_{\rm T}$.
Jaroslaw Kotowicz, Yatsuka Nakamura. Introduction to Go-Board -- Part I, Formalized Mathematics 3(1), pages 107-115, 1992. MML Identifier: GOBOARD1
Summary: In the article we introduce Go-board as some kinds of matrix which elements belong to topological space ${\cal E}^2_{\rm T}$. We define the functor of delaying column in Go-board and relation between Go-board and finite sequence of point from ${\cal E}^2_{\rm T}$. Basic facts about those notations are proved. The concept of the article is based on \cite{TAKE-NAKA}.
Jaroslaw Kotowicz, Yatsuka Nakamura. Introduction to Go-Board -- Part II, Formalized Mathematics 3(1), pages 117-121, 1992. MML Identifier: GOBOARD2
Summary: In article we define Go-board determined by finite sequence of points from topological space ${\cal E}^2_{\rm T}$. A few facts about this notation are proved.
Jaroslaw Kotowicz, Yatsuka Nakamura. Properties of Go-Board -- Part III, Formalized Mathematics 3(1), pages 123-124, 1992. MML Identifier: GOBOARD3
Summary: Two useful facts about Go-board are proved.
Jaroslaw Kotowicz, Yatsuka Nakamura. Go-Board Theorem, Formalized Mathematics 3(1), pages 125-129, 1992. MML Identifier: GOBOARD4
Summary: We prove the Go-board theorem which is a special case of Hex Theorem. The article is based on \cite{TAKE-NAKA}.
Waldemar Korczynski. Some Properties of Binary Relations, Formalized Mathematics 3(1), pages 131-134, 1992. MML Identifier: SYSREL
Summary: The article contains some theorems on binary relations, which are used in papers \cite{FF_SIEC.ABS}, \cite{E_SIEC.ABS}, \cite{S_SIEC.ABS}, and other.