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

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

Andrzej Trybulec. Tarski Grothendieck Set Theory, Formalized Mathematics 1(1), pages 9-11, 1990. MML Identifier: TARSKI
Summary: This is the first part of the axiomatics of the Mizar system. It includes the axioms of the Tarski Grothendieck set theory. They are: the axiom stating that everything is a set, the extensionality axiom, the definitional axiom of the singleton, the definitional axiom of the pair, the definitional axiom of the union of a family of sets, the definitional axiom of the boolean (the power set) of a set, the regularity axiom, the definitional axiom of the ordered pair, the Tarski's axiom~A introduced in \cite{TARSKI:1} (see also \cite{TARSKI:2}), and the Fr\ae nkel scheme. Also, the definition of equinumerosity is introduced.
Andrzej Trybulec. Built-in Concepts, Formalized Mathematics 1(1), pages 13-15, 1990. MML Identifier: AXIOMS
Summary: This abstract contains the second part of the axiomatics of the Mizar system (the first part is in abstract \cite{TARSKI.ABS}). The axioms listed here characterize the Mizar built-in concepts that are automatically attached to every Mizar article. We give definitional axioms of the following concepts: element, subset, Cartesian product, domain (non empty subset), subdomain (non empty subset of a domain), set domain (domain consisting of sets). Axioms of strong arithmetics of real numbers are also included.
Zinaida Trybulec, Halina Swiczkowska. Boolean Properties of Sets, Formalized Mathematics 1(1), pages 17-23, 1990. MML Identifier: BOOLE
Summary: This article contains proofs of the theorems which are obvious if the directive 'requirements BOOLE;' will be added to enviroment declaration of the Mizar article.
Andrzej Trybulec. Enumerated Sets, Formalized Mathematics 1(1), pages 25-34, 1990. MML Identifier: ENUMSET1
Summary: We prove basic facts about enumerated sets: definitional theorems and their immediate consequences, some theorems related to the decomposition of an enumerated set into union of two sets, facts about removing elements that occur more than once, and facts about permutations of enumerated sets (with the length $\le$ 4). The article includes also schemes enabling instantiation of up to nine universal quantifiers.
Krzysztof Hryniewiecki. Basic Properties of Real Numbers, Formalized Mathematics 1(1), pages 35-40, 1990. MML Identifier: REAL_1
Summary: Basic facts of arithmetics of real numbers are presented: definitions and properties of the complement element, the inverse element, subtraction and division; some basic properties of the set REAL (e.g. density), and the scheme of separation for sets of reals.
Grzegorz Bancerek. The Fundamental Properties of Natural Numbers, Formalized Mathematics 1(1), pages 41-46, 1990. MML Identifier: NAT_1
Summary: Some fundamental properties of addition, multiplication, order relations, exact division, the remainder, divisibility, the least common multiple, the greatest common divisor are presented. A proof of Euclid algorithm is also given.
Czeslaw Bylinski. Some Basic Properties of Sets, Formalized Mathematics 1(1), pages 47-53, 1990. MML Identifier: ZFMISC_1
Summary: In this article some basic theorems about singletons, pairs, power sets, unions of families of sets, and the cartesian product of two sets are proved.
Czeslaw Bylinski. Functions and Their Basic Properties, Formalized Mathematics 1(1), pages 55-65, 1990. MML Identifier: FUNCT_1
Summary: The definitions of the mode Function and the graph of a function are introduced. The graph of a function is defined to be identical with the function. The following concepts are also defined: the domain of a function, the range of a function, the identity function, the composition of functions, the 1-1 function, the inverse function, the restriction of a function, the image and the inverse image. Certain basic facts about functions and the notions defined in the article are proved.
Zinaida Trybulec. Properties of Subsets, Formalized Mathematics 1(1), pages 67-71, 1990. MML Identifier: SUBSET_1
Summary: The text includes theorems concerning properties of subsets, and some operations on sets. The functions yielding improper subsets of a set, i.e. the empty set and the set itself are introduced. Functions and predicates introduced for sets are redefined. Some theorems about enumerated sets are proved.
Edmund Woronowicz. Relations and Their Basic Properties, Formalized Mathematics 1(1), pages 73-83, 1990. MML Identifier: RELAT_1
Summary: We define here: mode Relation as a set of pairs, the domain, the codomain, and the field of relation; the empty and the identity relations, the composition of relations, the image and the inverse image of a set under a relation. Two predicates, = and $\subseteq$, and three functions, $\cup$, $\cap$ and $\setminus$ are redefined. Basic facts about the above mentioned notions are presented.
Edmund Woronowicz, Anna Zalewska. Properties of Binary Relations, Formalized Mathematics 1(1), pages 85-89, 1990. MML Identifier: RELAT_2
Summary: The paper contains definitions of some properties of binary relations: reflexivity, irreflexivity, symmetry, asymmetry, antisymmetry, connectedness, strong connectedness, and transitivity. Basic theorems relating the above mentioned notions are given.
Grzegorz Bancerek. The Ordinal Numbers, Formalized Mathematics 1(1), pages 91-96, 1990. MML Identifier: ORDINAL1
Summary: In the beginning of the article we show some consequences of the regularity axiom. In the second part we introduce the successor of a set and the notions of transitivity and connectedness wrt membership relation. Then we define ordinal numbers as transitive and connected sets, and we prove some theorems of them and of their sets. Lastly we introduce the concept of a transfinite sequence and we show transfinite induction and schemes of defining by transfinite induction.
Andrzej Trybulec. Tuples, Projections and Cartesian Products, Formalized Mathematics 1(1), pages 97-105, 1990. MML Identifier: MCART_1
Summary: The purpose of this article is to define projections of ordered pairs, and to introduce triples and quadruples, and their projections. The theorems in this paper may be roughly divided into two groups: theorems describing basic properties of introduced concepts and theorems related to the regularity, analogous to those proved for ordered pairs by Cz. Byli\'nski \cite{ZFMISC_1.ABS}. Cartesian products of subsets are redefined as subsets of Cartesian products.
Grzegorz Bancerek, Krzysztof Hryniewiecki. Segments of Natural Numbers and Finite Sequences, Formalized Mathematics 1(1), pages 107-114, 1990. MML Identifier: FINSEQ_1
Summary: We define the notion of an initial segment of natural numbers and prove a number of their properties. Using this notion we introduce finite sequences, subsequences, the empty sequence, a sequence of a domain, and the operation of concatenation of two sequences.
Andrzej Trybulec. Domains and Their Cartesian Products, Formalized Mathematics 1(1), pages 115-122, 1990. MML Identifier: DOMAIN_1
Summary: The article includes: theorems related to domains, theorems related to Cartesian products presented earlier in various articles and simplified here by substituting domains for sets and omitting the assumption that the sets involved must not be empty. Several schemes and theorems related to Fraenkel operator are given. We also redefine subset yielding functions such as the pair of elements of a set and the union of two subsets of a set.
Grzegorz Bancerek. The Well Ordering Relations, Formalized Mathematics 1(1), pages 123-129, 1990. MML Identifier: WELLORD1
Summary: Some theorems about well ordering relations are proved. The goal of the article is to prove that every two well ordering relations are either isomorphic or one of them is isomorphic to a segment of the other. The following concepts are defined: the segment of a relation induced by an element, well founded relations, well ordering relations, the restriction of a relation to a set, and the isomorphism of two relations. A number of simple facts is presented.
Grzegorz Bancerek. A Model of ZF Set Theory Language, Formalized Mathematics 1(1), pages 131-145, 1990. MML Identifier: ZF_LANG
Summary: The goal of this article is to construct a language of the ZF set theory and to develop a notational and conceptual base which facilitates a convenient usage of the language.
Beata Padlewska. Families of Sets, Formalized Mathematics 1(1), pages 147-152, 1990. MML Identifier: SETFAM_1
Summary: The article contains definitions of the following concepts: family of sets, family of subsets of a set, the intersection of a family of sets. Functors $\cup$, $\cap$, and $\setminus$ are redefined for families of subsets of a set. Some properties of these notions are presented.
Czeslaw Bylinski. Functions from a Set to a Set, Formalized Mathematics 1(1), pages 153-164, 1990. MML Identifier: FUNCT_2
Summary: The article is a continuation of \cite{FUNCT_1.ABS}. We define the following concepts: a function from a set $X$ into a set $Y$, denoted by ``Function of $X$,$Y$'', the set of all functions from a set $X$ into a set $Y$, denoted by Funcs($X$,$Y$), and the permutation of a set (mode Permutation of $X$, where $X$ is a set). Theorems and schemes included in the article are reformulations of the theorems of \cite{FUNCT_1.ABS} in the new terminology. Also some basic facts about functions of two variables are proved.
Agata Darmochwal. Finite Sets, Formalized Mathematics 1(1), pages 165-167, 1990. MML Identifier: FINSET_1
Summary: The article contains the definition of a finite set based on the notion of finite sequence. Some theorems about properties of finite sets and finite families of sets are proved.
Czeslaw Bylinski. Graphs of Functions, Formalized Mathematics 1(1), pages 169-173, 1990. MML Identifier: GRFUNC_1
Summary: The graph of a function is defined in \cite{FUNCT_1.ABS}. In this paper the graph of a function is redefined as a Relation. Operations on functions are interpreted as the corresponding operations on relations. Some theorems about graphs of functions are proved.
Czeslaw Bylinski. Binary Operations, Formalized Mathematics 1(1), pages 175-180, 1990. MML Identifier: BINOP_1
Summary: In this paper we define binary and unary operations on domains. We also define the following predicates concerning the operations: $\dots$ is commutative, $\dots$ is associative, $\dots$ is the unity of $\dots$, and $\dots$ is distributive wrt $\dots$. A number of schemes useful in justifying the existence of the operations are proved.
Edmund Woronowicz. Relations Defined on Sets, Formalized Mathematics 1(1), pages 181-186, 1990. MML Identifier: RELSET_1
Summary: The article includes theorems concerning properties of relations defined as a subset of the Cartesian product of two sets (mode Relation of $X$,$Y$ where $X$,$Y$ are sets). Some notions, introduced in \cite{RELAT_1.ABS} such as domain, codomain, field of a relation, composition of relations, image and inverse image of a set under a relation are redefined.
Andrzej Trybulec, Agata Darmochwal. Boolean Domains, Formalized Mathematics 1(1), pages 187-190, 1990. MML Identifier: FINSUB_1
Summary: BOOLE DOMAIN is a SET DOMAIN that is closed under union and difference. This condition is equivalent to being closed under symmetric difference and one of the following operations: union, intersection or difference. We introduce the set of all finite subsets of a set $A$, denoted by Fin $A$. The mode Finite Subset of a set $A$ is introduced with the mother type: Element of Fin $A$. In consequence, ``Finite Subset of \dots '' is an elementary type, therefore one may use such types as ``set of Finite Subset of $A$'', ``[(Finite Subset of $A$), Finite Subset of $A$]'', and so on. The article begins with some auxiliary theorems that belong really to \cite{BOOLE.ABS} or \cite{ORDINAL1.ABS} but are missing there. Moreover, bool $A$ is redefined as a SET DOMAIN, for an arbitrary set $A$.
Grzegorz Bancerek. Models and Satisfiability, Formalized Mathematics 1(1), pages 191-199, 1990. MML Identifier: ZF_MODEL
Summary: The article includes schemes of defining by structural induction, and definitions and theorems related to: the set of variables which have free occurrences in a ZF-formula, the set of all valuations of variables in a model, the set of all valuations which satisfy a ZF-formula in a model, the satisfiability of a ZF-formula in a model by a valuation, the validity of a ZF-formula in a model, the axioms of ZF-language, the model of the ZF set theory.
Grzegorz Bancerek. The Contraction Lemma, Formalized Mathematics 1(1), pages 201-203, 1990. MML Identifier: ZF_COLLA
Summary: The article includes the proof of the contraction lemma which claims that every class in which the axiom of extensionality is valid is isomorphic with a transitive class. In this article the isomorphism (wrt membership relation) of two sets is defined. It is based on \cite{MOST:1}.
Wojciech A. Trybulec. Axioms of Incidence, Formalized Mathematics 1(1), pages 205-213, 1990. MML Identifier: INCSP_1
Summary: This article is based on {\it ``Foundations of Geometry''} by Karol Borsuk and Wanda Szmielew (\cite{BORSUK:1}). The fourth axiom of incidence is weakened. In \cite{BORSUK:1} it has the form {\it for any plane there exist three non-collinear points in the plane} and in the article {\it for any plane there exists one point in the plane}. The original axiom is proved. The article includes: theorems concerning collinearity of points and coplanarity of points and lines, basic theorems concerning lines and planes, fundamental existence theorems, theorems concerning intersection of lines and planes.
Stanislaw Zukowski. Introduction to Lattice Theory, Formalized Mathematics 1(1), pages 215-222, 1990. MML Identifier: LATTICES
Summary: A lattice is defined as an algebra on a nonempty set with binary operations join and meet which are commutative and associative, and satisfy the absorption identities. The following kinds of lattices are considered: distributive, modular, bounded (with zero and unit elements), complemented, and Boolean (with complement). The article includes also theorems which immediately follow from definitions.
Beata Padlewska, Agata Darmochwal. Topological Spaces and Continuous Functions, Formalized Mathematics 1(1), pages 223-230, 1990. MML Identifier: PRE_TOPC
Summary: The paper contains a definition of topological space. The following notions are defined: point of topological space, subset of topological space, subspace of topological space, and continuous function.
Miroslaw Wysocki, Agata Darmochwal. Subsets of Topological Spaces, Formalized Mathematics 1(1), pages 231-237, 1990. MML Identifier: TOPS_1
Summary: The article contains some theorems about open and closed sets. The following topological operations on sets are defined: closure, interior and frontier. The following notions are introduced: dense set, boundary set, nowheredense set and set being domain (closed domain and open domain), and some basic facts concerning them are proved.
Beata Padlewska. Connected Spaces, Formalized Mathematics 1(1), pages 239-244, 1990. MML Identifier: CONNSP_1
Summary: The following notions are defined: separated sets, connected spaces, connected sets, components of a topological space, the component of a point. The definition of the boundary of a set is also included. The singleton of a point of a topological space is redefined as a subset of the space. Some theorems about these notions are proved.
Czeslaw Bylinski. Basic Functions and Operations on Functions, Formalized Mathematics 1(1), pages 245-254, 1990. MML Identifier: FUNCT_3
Summary: We define the following mappings: the characteristic function of a subset of a set, the inclusion function (injection or embedding), the projections from a Cartesian product onto its arguments and diagonal function (inclusion of a set into its Cartesian square). Some operations on functions are also defined: the products of two functions (the complex function and the more general product-function), the function induced on power sets by the image and inverse-image. Some simple propositions related to the introduced notions are proved.