Kanchun
  1. Kanchun , Yatsuka Nakamura. The Inner Product of Finite Sequences and of Points of $n$-dimensional Topological Space, Formalized Mathematics 11(2), pages 179-183, 2003. MML Identifier: EUCLID_2
    Summary: First, we define the inner product to finite sequences of real value. Next, we extend it to points of $n$-dimensional topological space ${\calE}^{n}_{\rmT}$. At the end, orthogonality is introduced to this space.
  2. Kanchun , Hiroshi Yamazaki, Yatsuka Nakamura. Cross Products and Tripple Vector Products in 3-dimensional Euclidean Space, Formalized Mathematics 11(4), pages 381-383, 2003. MML Identifier: EUCLID_5
    Summary: First, we extend the basic theorems of 3-dimensional euclidian space, and then define the cross product in the same space and relative vector relations using the above definition.
Mitsuru Aoki
  1. Grzegorz Bancerek, Mitsuru Aoki, Akio Matsumoto, Yasunari Shidama. Processes in Petri nets, Formalized Mathematics 11(1), pages 125-132, 2003. MML Identifier: PNPROC_1
    Summary: Sequential and concurrent compositions of processes in Petri nets are introduced. A process is formalized as a set of (possible), so called, firing sequences. In the definition of the sequential composition the standard concatenation is used $$ R_1 \mathop{\rm before} R_2 = \{p_1\mathop{^\frown}p_2: p_1\in R_1\ \land\ p_2\in R_2\} $$ The definition of the concurrent composition is more complicated $$ R_1 \mathop{\rm concur} R_2 = \{ q_1\cup q_2: q_1\ {\rm misses}\ q_2\ \land\ \mathop{\rm Seq} q_1\in R_1\ \land\ \mathop{\rm Seq} q_2\in R_2\} $$ For example, $$ \{\langle t_0\rangle\} \mathop{\rm concur} \{\langle t_1,t_2\rangle\} = \{\langle t_0,t_1,t_2\rangle , \langle t_1,t_0,t_2\rangle , \langle t_1,t_2,t_0\rangle\} $$ The basic properties of the compositions are shown.
William W. Armstrong
  1. William W. Armstrong, Yatsuka Nakamura, Piotr Rudnicki. Armstrong's Axioms, Formalized Mathematics 11(1), pages 39-51, 2003. MML Identifier: ARMSTRNG
    Summary: We present a formalization of the seminal paper by W.~W.~Armstrong~\cite{arm74} on functional dependencies in relational data bases. The paper is formalized in its entirety including examples and applications. The formalization was done with a routine effort albeit some new notions were defined which simplified formulation of some theorems and proofs.\par The definitive reference to the theory of relational databases is~\cite{Maier}, where saturated sets are called closed sets. Armstrong's ``axioms'' for functional dependencies are still widely taught at all levels of database design, see for instance~\cite{Elmasri}.
Broderick Arneson
  1. Broderick Arneson, Piotr Rudnicki. Primitive Roots of Unity and Cyclotomic Polynomials, Formalized Mathematics 12(1), pages 59-67, 2004. MML Identifier: UNIROOTS
    Summary: We present a formalization of roots of unity, define cyclotomic polynomials and demonstrate the relationship between cyclotomic polynomials and unital polynomials.
  2. Broderick Arneson, Matthias Baaz, Piotr Rudnicki. Witt's Proof of the Wedderburn Theorem, Formalized Mathematics 12(1), pages 69-75, 2004. MML Identifier: WEDDWITT
    Summary: We present a formalization of Witt's proof of the Wedderburn theorem following Chapter 5 of {\em Proofs from THE BOOK} by Martin Aigner and G\"{u}nter M. Ziegler, 2nd ed., Springer 1999.
  3. Broderick Arneson, Piotr Rudnicki. Chordal Graphs, Formalized Mathematics 14(3), pages 79-92, 2006. MML Identifier: CHORD
    Summary: We are formalizing \cite[pp.~81--84]{Golumbic} where chordal graphs are defined and their basic characterization is given. This formalization is a part of the M.Sc. work of the first author under supervision of the second author.
  4. Broderick Arneson, Piotr Rudnicki. Recognizing Chordal Graphs: Lex BFS and MCS, Formalized Mathematics 14(4), pages 187-205, 2006. MML Identifier: LEXBFS
    Summary: We are formalizing the algorithm for recognizing chordal graphs by lexicographic breadth-first search as presented in \cite[Section 3 of Chapter4, pp.~81--84]{Golumbic}. Then we follow with a formalization of another algorithm serving the same end but based on maximum cardinality search as presented by Tarjan and Yannakakis~\cite{TY84}.\par This work is a part of the MSc work of the first author under supervision of the second author. We would like to thank one of the anonymous reviewers for very useful suggestions.
Noriko Asamoto
  1. Noriko Asamoto. Some Multi Instructions Defined by Sequence of Instructions of \SCMFSA, Formalized Mathematics 5(4), pages 615-619, 1996. MML Identifier: SCMFSA_7
    Summary:
  2. Andrzej Trybulec, Yatsuka Nakamura, Noriko Asamoto. On the Compositions of Macro Instructions. Part I, Formalized Mathematics 6(1), pages 21-27, 1997. MML Identifier: SCMFSA6A
    Summary:
  3. Noriko Asamoto, Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec. On the Composition of Macro Instructions. Part II, Formalized Mathematics 6(1), pages 41-47, 1997. MML Identifier: SCMFSA6B
    Summary: We define the semantics of macro instructions (introduced in \cite{SCMFSA6A.ABS}) in terms of executions of ${\bf SCM}_{\rm FSA}$. In a similar way, we define the semantics of macro composition. Several attributes of macro instructions are introduced (paraclosed, parahalting, keeping 0) and their usage enables a systematic treatment of the composition of macro intructions. This article is continued in \cite{SCMFSA6C.ABS}.
  4. Noriko Asamoto, Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec. On the Composition of Macro Instructions. Part III, Formalized Mathematics 6(1), pages 53-57, 1997. MML Identifier: SCMFSA6C
    Summary: This article is a continuation of \cite{SCMFSA6A.ABS} and \cite{SCMFSA6C.ABS}. First, we recast the semantics of the macro composition in more convenient terms. Then, we introduce terminology and basic properties of macros constructed out of single instructions of ${\bf SCM}_{\rm FSA}$. We give the complete semantics of composing a macro instruction with an instruction and for composing two machine instructions (this is also done in terms of macros). The introduced terminology is tested on the simple example of a macro for swapping two integer locations.
  5. Noriko Asamoto. Constant Assignment Macro Instructions of \SCMFSA. Part II, Formalized Mathematics 6(1), pages 59-63, 1997. MML Identifier: SCMFSA7B
    Summary:
  6. Noriko Asamoto. Conditional Branch Macro Instructions of \SCMFSA. Part I, Formalized Mathematics 6(1), pages 65-72, 1997. MML Identifier: SCMFSA8A
    Summary:
  7. Noriko Asamoto. Conditional Branch Macro Instructions of \SCMFSA. Part II, Formalized Mathematics 6(1), pages 73-80, 1997. MML Identifier: SCMFSA8B
    Summary:
  8. Noriko Asamoto. The loop and Times Macroinstruction for \SCMFSA, Formalized Mathematics 6(4), pages 483-497, 1997. MML Identifier: SCMFSA8C
    Summary: We implement two macroinstructions {\tt loop} and {\tt Times} which iterate macroinstructions of {\SCMFSA}. In a {\tt loop} macroinstruction it jumps to the head when the original macroinstruction stops, in a {\tt Times} macroinstruction it behaves as if the original macroinstruction repeats $n$ times.
Matthias Baaz
  1. Broderick Arneson, Matthias Baaz, Piotr Rudnicki. Witt's Proof of the Wedderburn Theorem, Formalized Mathematics 12(1), pages 69-75, 2004. MML Identifier: WEDDWITT
    Summary: We present a formalization of Witt's proof of the Wedderburn theorem following Chapter 5 of {\em Proofs from THE BOOK} by Martin Aigner and G\"{u}nter M. Ziegler, 2nd ed., Springer 1999.
Jonathan Backer
  1. Jonathan Backer, Piotr Rudnicki, Christoph Schwarzweller. Ring Ideals, Formalized Mathematics 9(3), pages 565-582, 2001. MML Identifier: IDEAL_1
    Summary: We introduce the basic notions of ideal theory in rings. This includes left and right ideals, (finitely) generated ideals and some operations on ideals such as the addition of ideals and the radical of an ideal. In addition we introduce linear combinations to formalize the well-known characterization of generated ideals. Principal ideal domains and Noetherian rings are defined. The latter development follows \cite{Becker93}, pages 144--145.
  2. Jonathan Backer, Piotr Rudnicki. Hilbert Basis Theorem, Formalized Mathematics 9(3), pages 583-589, 2001. MML Identifier: HILBASIS
    Summary: We prove the Hilbert basis theorem following \cite{Becker93}, page 145. First we prove the theorem for the univariate case and then for the multivariate case. Our proof for the latter is slightly different than in \cite{Becker93}. As a base case we take the ring of polynomilas with no variables. We also prove that a polynomial ring with infinite number of variables is not Noetherian.
Lilla Krystyna Baginska
  1. Lilla Krystyna Baginska, Adam Grabowski. On the Kuratowski Closure-Complement Problem, Formalized Mathematics 11(3), pages 323-329, 2003. MML Identifier: KURATO_1
    Summary: In this article we formalize the Kuratowski closure-complement result: there is at most 14 distinct sets that one can produce from a given subset $A$ of a topological space $T$ by applying closure and complement operators and that all 14 can be obtained from a suitable subset of $\Bbb R,$ namely KuratExSet $=\{1\} \cup {\Bbb Q} (2,3) \cup (3, 4)\cup (4,\infty)$.\par The second part of the article deals with the maximal number of distinct sets which may be obtained from a given subset $A$ of $T$ by applying closure and interior operators. The subset KuratExSet of $\Bbb R$ is also enough to show that 7 can be achieved.
Agnieszka Banachowicz
  1. Agnieszka Banachowicz, Anna Winnicka. Complex Sequences, Formalized Mathematics 4(1), pages 121-124, 1993. MML Identifier: COMSEQ_1
    Summary: Definitions of complex sequence and operations on sequences (multiplication of sequences and multiplication by a complex number, addition, subtraction, division and absolute value of sequence) are given. We followed \cite{SEQ_1.ABS}.
Grzegorz Bancerek
  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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}.
  8. Grzegorz Bancerek. Zermelo Theorem and Axiom of Choice, Formalized Mathematics 1(2), pages 265-267, 1990. MML Identifier: WELLORD2
    Summary: The article is continuation of \cite{WELLORD1.ABS} and \cite{ORDINAL1.ABS}, and the goal of it is show that Zermelo theorem (every set has a relation which well orders it - proposition (26)) and axiom of choice (for every non-empty family of non-empty and separate sets there is set which has exactly one common element with arbitrary family member - proposition (27)) are true. It is result of the Tarski's axiom A introduced in \cite{TARSKI:1} and repeated in \cite{TARSKI.ABS}. Inclusion as a settheoretical binary relation is introduced, the correspondence of well ordering relations to ordinal numbers is shown, and basic properties of equinumerosity are presented. Some facts are based on \cite{KURAT-MOST:1}.
  9. Grzegorz Bancerek. Properties of ZF Models, Formalized Mathematics 1(2), pages 277-280, 1990. MML Identifier: ZFMODEL1
    Summary: The article deals with the concepts of satisfiability of ZF set theory language formulae in a model (a non-empty family of sets) and the axioms of ZF theory introduced in \cite{MOST:1}. It is shown that the transitive model satisfies the axiom of extensionality and that it satisfies the axiom of pairs if and only if it is closed to pair operation; it satisfies the axiom of unions if and only if it is closed to union operation, etc. The conditions which are satisfied by arbitrary model of ZF set theory are also shown. Besides introduced are definable and parametrically definable functions.
  10. Grzegorz Bancerek. Sequences of Ordinal Numbers, Formalized Mathematics 1(2), pages 281-290, 1990. MML Identifier: ORDINAL2
    Summary: In the first part of the article we introduce the following operations: On $X$ that yields the set of all ordinals which belong to the set $X$, Lim $X$ that yields the set of all limit ordinals which belong to $X$, and inf $X$ and sup $X$ that yield the minimal ordinal belonging to $X$ and the minimal ordinal greater than all ordinals belonging to $X$, respectively. The second part of the article starts with schemes that can be used to justify the correctness of definitions based on the transfinite induction (see \cite{ORDINAL1.ABS} or \cite{KURAT-MOST:1}). The schemes are used to define addition, product and power of ordinal numbers. The operations of limes inferior and limes superior of sequences of ordinals are defined and the concepts of limit of ordinal sequence and increasing and continuous sequence are introduced.
  11. Grzegorz Bancerek. Cardinal Numbers, Formalized Mathematics 1(2), pages 377-382, 1990. MML Identifier: CARD_1
    Summary: We present the choice function rule in the beginning of the article. In the main part of the article we formalize the base of cardinal theory. In the first section we introduce the concept of cardinal numbers and order relations between them. We present here Cantor-Bernstein theorem and other properties of order relation of cardinals. In the second section we show that every set has cardinal number equipotence to it. We introduce notion of alephs and we deal with the concept of finite set. At the end of the article we show two schemes of cardinal induction. Some definitions are based on \cite{GUZ-ZBIER:1} and \cite{KURAT-MOST:1}.
  12. Wojciech A. Trybulec, Grzegorz Bancerek. Kuratowski -- Zorn Lemma, Formalized Mathematics 1(2), pages 387-393, 1990. MML Identifier: ORDERS_2
    Summary: The goal of this article is to prove Kuratowski - Zorn lemma. We prove it in a number of forms (theorems and schemes). We introduce the following notions: a relation is a quasi (or partial, or linear) order, a relation quasi (or partially, or linearly) orders a set, minimal and maximal element in a relation, inferior and superior element of a relation, a set has lower (or upper) Zorn property w.r.t. a relation. We prove basic theorems concerning those notions and theorems that relate them to the notions introduced in \cite{ORDERS_1.ABS}. At the end of the article we prove some theorems that belong rather to \cite{RELAT_1.ABS}, \cite{RELAT_2.ABS} or \cite{WELLORD1.ABS}.
  13. Grzegorz Bancerek. Introduction to Trees, Formalized Mathematics 1(2), pages 421-427, 1990. MML Identifier: TREES_1
    Summary: The article consists of two parts: the first one deals with the concept of the prefixes of a finite sequence, the second one introduces and deals with the concept of tree. Besides some auxiliary propositions concerning finite sequences are presented. The trees are introduced as non-empty sets of finite sequences of natural numbers which are closed on prefixes and on sequences of less numbers (i.e. if $\langle n_1$, $n_2$, $\dots$, $n_k\rangle$ is a vertex (element) of a tree and $m_i \leq n_i$ for $i = 1$, $2$, $\dots$, $k$, then $\langle m_1$, $m_2$, $\dots$, $m_k\rangle$ also is). Finite trees, elementary trees with $n$ leaves, the leaves and the subtrees of a tree, the inserting of a tree into another tree, with a node used for determining the place of insertion, antichains of prefixes, and height and width of finite trees are introduced.
  14. Grzegorz Bancerek. Connectives and Subformulae of the First Order Language, Formalized Mathematics 1(3), pages 451-458, 1990. MML Identifier: QC_LANG2
    Summary: In the article the development of the first order language defined in \cite{QC_LANG1.ABS} is continued. The following connectives are introduced: implication ($\Rightarrow$), disjunction ($\vee$), and equivalence ($\Leftrightarrow$). We introduce also the existential quantifier ($\exists$) and FALSUM. Some theorems on disjunctive, conditional, biconditional and existential formulae are proved and their selector functors are introduced. The second part of the article deals with notions of subformula, proper subformula and immediate constituent of a QC-formula.
  15. Czeslaw Bylinski, Grzegorz Bancerek. Variables in Formulae of the First Order Language, Formalized Mathematics 1(3), pages 459-469, 1990. MML Identifier: QC_LANG3
    Summary: We develop the first order language defined in \cite{QC_LANG1.ABS}. We continue the work done in the article \cite{QC_LANG2.ABS}. We prove some schemes of defining by structural induction. We deal with notions of closed subformulae and of still not bound variables in a formula. We introduce the concept of the set of all free variables and the set of all fixed variables occurring in a formula.
  16. Grzegorz Bancerek. Ordinal Arithmetics, Formalized Mathematics 1(3), pages 515-519, 1990. MML Identifier: ORDINAL3
    Summary: At the beginning the article contains some auxiliary theorems concerning the constructors defined in papers \cite{ORDINAL1.ABS} and \cite{ORDINAL2.ABS}. Next simple properties of addition and multiplication of ordinals are shown, e.g. associativity of addition. Addition and multiplication of a transfinite sequence of ordinals and a ordinal are also introduced here. The goal of the article is the proof that the distributivity of multiplication wrt addition and the associativity of multiplication hold. Additionally new binary functors of ordinals are introduced: subtraction, exact division, and remainder and some of their basic properties are presented.
  17. Grzegorz Bancerek. Curried and Uncurried Functions, Formalized Mathematics 1(3), pages 537-541, 1990. MML Identifier: FUNCT_5
    Summary: In the article following functors are introduced: the projections of subsets of the Cartesian product, the functor which for every function $f:X \times Y \to Z$ gives some curried function ($X \to(Y \to Z)$), and the functor which from curried functions makes uncurried functions. Some of their properties and some properties of the set of all functions from a set into a set are also shown.
  18. Grzegorz Bancerek. Cardinal Arithmetics, Formalized Mathematics 1(3), pages 543-547, 1990. MML Identifier: CARD_2
    Summary: In the article addition, multiplication and power operation of cardinals are introduced. Presented are some properties of equipotence of Cartesian products, basic cardinal arithmetics laws (transformativity, associativity, distributivity), and some facts about finite sets.
  19. Grzegorz Bancerek. Tarski's Classes and Ranks, Formalized Mathematics 1(3), pages 563-567, 1990. MML Identifier: CLASSES1
    Summary: In the article the Tarski's classes (non-empty families of sets satisfying Tarski's axiom A given in \cite{TARSKI.ABS}) and the rank sets are introduced and some of their properties are shown. The transitive closure and the rank of a set is given here too.
  20. Grzegorz Bancerek. K\"onig's Theorem, Formalized Mathematics 1(3), pages 589-593, 1990. MML Identifier: CARD_3
    Summary: In the article the sum and product of any number of cardinals are introduced and their relationships to addition, multiplication and to other concepts are shown. Then the K\"onig's theorem is proved. The theorem that the cardinal of union of increasing family of sets of power less than some cardinal {\bf m} is not greater than {\bf m}, is given too.
  21. Bogdan Nowak, Grzegorz Bancerek. Universal Classes, Formalized Mathematics 1(3), pages 595-600, 1990. MML Identifier: CLASSES2
    Summary: In the article we have shown that there exist universal classes, i.e. there are sets which are closed w.r.t. basic set theory operations.
  22. Grzegorz Bancerek. Increasing and Continuous Ordinal Sequences, Formalized Mathematics 1(4), pages 711-714, 1990. MML Identifier: ORDINAL4
    Summary: Concatenation of two ordinal sequences, the mode of all ordinals belonging to a universe and the mode of sequences of them with length equal to the rank of the universe are introduced. Besides, the increasing and continuous transfinite sequences, the limes of ordinal sequences and the power of ordinals, and the fact that every increasing and continuous transfinite sequence has critical numbers (fixed points) are discussed.
  23. Grzegorz Bancerek. Filters -- Part I, Formalized Mathematics 1(5), pages 813-819, 1990. MML Identifier: FILTER_0
    Summary: Filters of a lattice, maximal filters (ultrafilters), operation to create a filter generating by an element or by a non-empty subset of the lattice are discussed. Besides, there are introduced implicative lattices such that for every two elements there is an element being pseudo-complement of them. Some facts concerning these concepts are presented too, i.e. for any proper filter there exists an ultrafilter consisting it.
  24. Grzegorz Bancerek. Replacing of Variables in Formulas of ZF Theory, Formalized Mathematics 1(5), pages 963-972, 1990. MML Identifier: ZF_LANG1
    Summary: Part one is a supplement to papers \cite{ZF_LANG.ABS}, \cite{ZF_MODEL.ABS}, and \cite{ZFMODEL1.ABS}. It deals with concepts of selector functions, atomic, negative, conjunctive formulas and etc., subformulas, free variables, satisfiability and models (it is shown that axioms of the predicate and the quantifier calculus are satisfied in an arbitrary set). In part two there are introduced notions of variables occurring in a formula and replacing of variables in a formula.
  25. Grzegorz Bancerek. The Reflection Theorem, Formalized Mathematics 1(5), pages 973-977, 1990. MML Identifier: ZF_REFLE
    Summary: The goal is show that the reflection theorem holds. The theorem is as usual in the Morse-Kelley theory of classes (MK). That theory works with universal class which consists of all sets and every class is a subclass of it. In this paper (and in another Mizar articles) we work in Tarski-Grothendieck (TG) theory (see \cite{TARSKI.ABS}) which ensures the existence of sets that have properties like universal class (i.e. this theory is stronger than MK). The sets are introduced in \cite{CLASSES2.ABS} and some concepts of MK are modeled. The concepts are: the class $On$ of all ordinal numbers belonging to the universe, subclasses, transfinite sequences of non-empty elements of universe, etc. The reflection theorem states that if $A_\xi$ is an increasing and continuous transfinite sequence of non-empty sets and class $A = \bigcup_{\xi \in On} A_\xi$, then for every formula $H$ there is a strictly increasing continuous mapping $F: On \to On$ such that if $\varkappa$ is a critical number of $F$ (i.e. $F(\varkappa) = \varkappa > 0$) and $f \in A_\varkappa^{\bf VAR}$, then $A,f\models H \equiv\ {A_\varkappa},f\models H$. The proof is based on \cite{MOST:1}. Besides, in the article it is shown that every universal class is a model of ZF set theory if $\omega$ (the first infinite ordinal number) belongs to it. Some propositions concerning ordinal numbers and sequences of them are also present.
  26. Grzegorz Bancerek. Consequences of the Reflection Theorem, Formalized Mathematics 1(5), pages 989-993, 1990. MML Identifier: ZFREFLE1
    Summary: Some consequences of the reflection theorem are discussed. To formulate them the notions of elementary equivalence and subsystems, and of models for a set of formulae are introduced. Besides, the concept of cofinality of a ordinal number with second one is used. The consequences of the reflection theorem (it is sometimes called the Scott-Scarpellini lemma) are: (i) If $A_\xi$ is a transfinite sequence as in the reflection theorem (see \cite{ZF_REFLE.ABS}) and $A = \bigcup_{\xi \in On} A_\xi$, then there is an increasing and continuous mapping $\phi$ from $On$ into $On$ such that for every critical number $\kappa$ the set $A_\kappa$ is an elementary subsystem of $A$ ($A_\kappa \prec A$). (ii) There is an increasing continuous mapping $\phi: On \to On$ such that ${\bf R}_\kappa \prec V$ for each of its critical numbers $\kappa$ ($V$ is the universal class and $On$ is the class of all ordinals belonging to $V$). (iii) There are ordinal numbers $\alpha$ cofinal with $\omega$ for which ${\bf R}_\alpha$ are models of ZF set theory. (iv) For each set $X$ from universe $V$ there is a model of ZF $M$ which belongs to $V$ and has $X$ as an element.
  27. Grzegorz Bancerek. Countable Sets and Hessenberg's Theorem, Formalized Mathematics 2(1), pages 65-69, 1991. MML Identifier: CARD_4
    Summary: The concept of countable sets is introduced and there are shown some facts which deal with finite and countable sets. Besides, the article includes theorems and lemmas on the sum and product of infinite cardinals. The most important of them is Hessenberg's theorem which says that for every infinite cardinal {\bf m} the product ${\bf m} \cdot {\bf m}$ is equal to {\bf m}.
  28. Grzegorz Bancerek. Definable Functions, Formalized Mathematics 2(1), pages 143-145, 1991. MML Identifier: ZFMODEL2
    Summary: The article is continuation of \cite{ZF_LANG1.ABS} and \cite{ZFMODEL1.ABS}. It deals with concepts of variables occurring in a formula and free variables, replacing of variables in a formula and definable functions. The goal of it is to create a base of facts which are neccesary to show that every model of ZF set theory is a good model, i.e. it is closed with respect to fundamental settheoretical operations (union, intersection, Cartesian product etc.). The base includes the facts concerning with the composition and conditional sum of two definable functions.
  29. Grzegorz Bancerek, Agata Darmochwal, Andrzej Trybulec. Propositional Calculus, Formalized Mathematics 2(1), pages 147-150, 1991. MML Identifier: LUKASI_1
    Summary: We develop the classical propositional calculus, following \cite{LUKA:1}.
  30. Grzegorz Bancerek. K\"onig's Lemma, Formalized Mathematics 2(3), pages 397-402, 1991. MML Identifier: TREES_2
    Summary: A continuation of \cite{TREES_1.ABS}. The notion of finite--order trees, succesors of an element of a tree, and chains, levels and branches of a tree are introduced. That notion has been used to formalize K\"onig's Lemma which claims that there is a infinite branch of a finite-order tree if the tree has arbitrary long finite chains. Besides, the concept of decorated trees is introduced and some concepts dealing with trees are applied to decorated trees.
  31. Grzegorz Bancerek, Andrzej Kondracki. Mostowski's Fundamental Operations -- Part II, Formalized Mathematics 2(3), pages 425-427, 1991. MML Identifier: ZF_FUND2
    Summary: The article consists of two parts. The first part is translation of chapter II.3 of \cite{MOST:1}. A section of $D_{H}(a)$ determined by $f$ (symbolically $S_{H}(a,f)$) and a notion of predicative closure of a class are defined. It is proved that if following assumptions are satisfied: (o) $A=\bigcup_{\xi}A_{\xi}$, (i) $A_{\xi} \subset A_{\eta}$ for $\xi < \eta$, (ii) $A_{\lambda}=\bigcup_{\xi<\lambda}A_{\lambda}$ ($\lambda$ is a limit number), (iii) $A_{\xi}\in A$, (iv) $A_{\xi}$ is transitive, (v) $(x,y\in A) \rightarrow (x\cap y\in A)$, (vi) $A$ is predicatively closed, then the axiom of power sets and the axiom of substitution are valid in $A$. The second part is continuation of \cite{ZF_FUND1.ABS}. It is proved that if a non-void, transitive class is closed with respect to the operations $A_{1}-A_{7}$ then it is predicatively closed. At last sufficient criteria for a class to be a model of ZF-theory are formulated: if $A_{\xi}$ satisfies o -- iv and $A$ is closed under the operations $A_{1}-A_{7}$ then $A$ is a model of ZF.
  32. Grzegorz Bancerek. Filters -- Part II. Quotient Lattices Modulo Filters and Direct Product of Two Lattices, Formalized Mathematics 2(3), pages 433-438, 1991. MML Identifier: FILTER_1
    Summary: Binary and unary operation preserving binary relations and quotients of those operations modulo equivalence relations are introduced. It is shown that the quotients inherit some important properties (commutativity, associativity, distributivity, etc.). Based on it, the quotient (also called factor) lattice modulo a filter (i.e. modulo the equivalence relation w.r.t the filter) is introduced. Similarly, some properties of the direct product of two binary (unary) operations are present and then the direct product of two lattices is introduced. Besides, the heredity of distributivity, modularity, completeness, etc., for the product of lattices is also shown. Finally, the concept of isomorphic lattices is introduced, and there is shown that every Boolean lattice $B$ is isomorphic with the direct product of the factor lattice $B/[a]$ and the lattice latt$[a]$, where $a$ is an element of $B$.
  33. Grzegorz Bancerek. Cartesian Product of Functions, Formalized Mathematics 2(4), pages 547-552, 1991. MML Identifier: FUNCT_6
    Summary: A supplement of \cite{CARD_3.ABS} and \cite{FUNCT_5.ABS}, i.e. some useful and explanatory properties of the product and also the curried and uncurried functions are shown. Besides, the functions yielding functions are considered: two different products and other operation of such functions are introduced. Finally, two facts are presented: quasi-distributivity of the power of the set to other one w.r.t. the union ($X^{\biguplus_{x}f(x)} \approx \prod_{x}X^{f(x)}$) and quasi-distributivity of the product w.r.t. the raising to the power ($\prod_{x}{f(x)^X} \approx (\prod_{x}f(x))^X$).
  34. Grzegorz Bancerek, Agata Darmochwal. Comma Category, Formalized Mathematics 2(5), pages 679-681, 1991. MML Identifier: COMMACAT
    Summary: Comma category of two functors is introduced.
  35. Patricia L. Carlson, Grzegorz Bancerek. Context-Free Grammar -- Part 1, Formalized Mathematics 2(5), pages 683-687, 1991. MML Identifier: LANG1
    Summary: The concept of context-free grammar and of derivability in grammar are introduced. Moreover, the language (set of finite sequences of symbols) generated by grammar and some grammars are defined. The notion convenient to prove facts on language generated by grammar with exchange of symbols on grammar of union and concatenation of languages is included.
  36. Grzegorz Bancerek. Complete Lattices, Formalized Mathematics 2(5), pages 719-725, 1991. MML Identifier: LATTICE3
    Summary: In the first section the lattice of subsets of distinct set is introduced. The join and meet operations are, respectively, union and intersection of sets, and the ordering relation is inclusion. It is shown that this lattice is Boolean, i.e. distributive and complementary. The second section introduces the poset generated in a distinct lattice by its ordering relation. Besides, it is proved that posets which have l.u.b.'s and g.l.b.'s for every two elements generate lattices with the same ordering relations. In the last section the concept of complete lattice is introduced and discussed. Finally, the fact that the function $f$ from subsets of distinct set yielding elements of this set is a infinite union of some complete lattice, if $f$ yields an element $a$ for singleton $\{a\}$ and $f(f^\circ X) = f(\bigsqcup X)$ for every subset $X$, is proved. Some concepts and proofs are based on \cite{RASIOWA-SIKOR} and \cite{TRACZYK}.
  37. 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}.
  38. 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.
  39. 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.
  40. 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$.
  41. 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.
  42. Grzegorz Bancerek, Piotr Rudnicki. Development of Terminology for \bf SCM, Formalized Mathematics 4(1), pages 61-67, 1993. MML Identifier: SCM_1
    Summary: We develop a higher level terminology for the {\bf SCM} machine defined by Nakamura and Trybulec in \cite{AMI_1.ABS}. Among numerous technical definitions and lemmas we define a complexity measure of a halting state of {\bf SCM} and a loader for {\bf SCM} for arbitrary finite sequence of instructions. In order to test the introduced terminology we discuss properties of eight shortest halting programs, one for each instruction.
  43. Grzegorz Bancerek, Piotr Rudnicki. Two Programs for \bf SCM. Part I -- Preliminaries, Formalized Mathematics 4(1), pages 69-72, 1993. MML Identifier: PRE_FF
    Summary: In two articles (this one and \cite{FIB_FUSC.ABS}) we discuss correctness of two short programs for the {\bf SCM} machine: one computes Fibonacci numbers and the other computes the {\em fusc} function of Dijkstra \cite{DIJKSTRA}. The limitations of current Mizar implementation rendered it impossible to present the correctness proofs for the programs in one article. This part is purely technical and contains a number of very specific lemmas about integer division, floor, exponentiation and logarithms. The formal definitions of the Fibonacci sequence and the {\em fusc} function may be of general interest.
  44. Grzegorz Bancerek, Piotr Rudnicki. Two Programs for \bf SCM. Part II -- Programs, Formalized Mathematics 4(1), pages 73-75, 1993. MML Identifier: FIB_FUSC
    Summary: We prove the correctness of two short programs for the {\bf SCM} machine: one computes Fibonacci numbers and the other computes the {\em fusc} function of Dijkstra \cite{DIJKSTRA}. The formal definitions of these functions can be found in \cite{PRE_FF.ABS}. We prove the total correctness of the programs in two ways: by conducting inductions on computations and inductions on input data. In addition we characterize the concrete complexity of the programs as defined in \cite{SCM_1.ABS}.
  45. Grzegorz Bancerek. Joining of Decorated Trees, Formalized Mathematics 4(1), pages 77-82, 1993. MML Identifier: TREES_4
    Summary: This is the continuation of the sequence of articles on trees (see \cite{TREES_1.ABS}, \cite{TREES_2.ABS}, \cite{TREES_3.ABS}). The main goal is to introduce joining operations on decorated trees corresponding with operations introduced in \cite{TREES_3.ABS}. We will also introduce the operation of substitution. In the last section we dealt with trees decorated by Cartesian product, i.e. we showed some lemmas on joining operations applied to such trees.
  46. Grzegorz Bancerek, Piotr Rudnicki. On Defining Functions on Trees, Formalized Mathematics 4(1), pages 91-101, 1993. MML Identifier: DTCONSTR
    Summary: The continuation of the sequence of articles on trees (see \cite{TREES_1.ABS}, \cite{TREES_2.ABS}, \cite{TREES_3.ABS}, \cite{TREES_4.ABS}) and on context-free grammars (\cite{LANG1.ABS}). We define the set of complete parse trees for a given context-free grammar. Next we define the scheme of induction for the set and the scheme of defining functions by induction on the set. For each symbol of a context-free grammar we define the terminal, the pretraversal, and the posttraversal languages. The introduced terminology is tested on the example of Peano naturals.
  47. Grzegorz Bancerek, Piotr Rudnicki. On Defining Functions on Binary Trees, Formalized Mathematics 5(1), pages 9-13, 1996. MML Identifier: BINTREE1
    Summary: This article is a continuation of an article on defining functions on trees (see \cite{DTCONSTR.ABS}). In this article we develop terminology specialized for binary trees, first defining binary trees and binary grammars. We recast the induction principle for the set of parse trees of binary grammars and the scheme of defining functions inductively with the set as domain. We conclude with defining the scheme of defining such functions by lambda-like expressions.
  48. Grzegorz Bancerek, Piotr Rudnicki. A Compiler of Arithmetic Expressions for SCM, Formalized Mathematics 5(1), pages 15-20, 1996. MML Identifier: SCM_COMP
    Summary: We define a set of binary arithmetic expressions with the following operations: $+$, $-$, $\cdot$, {\tt mod}, and {\tt div} and formalize the common meaning of the expressions in the set of integers. Then, we define a compile function that for a given expression results in a program for the {\bf SCM} machine defined by Nakamura and Trybulec in \cite{AMI_1.ABS}. We prove that the generated program when loaded into the machine and executed computes the value of the expression. The program uses additional memory and runs in time linear in length of the expression.
  49. Grzegorz Bancerek. Quantales, Formalized Mathematics 5(1), pages 85-91, 1996. MML Identifier: QUANTAL1
    Summary: The concepts of Girard quantales (see \cite{GIRARD:TCS50} and \cite{YETTER}) and Blikle nets (see \cite{BLIKLE}) are introduced.
  50. Grzegorz Bancerek. Ideals, Formalized Mathematics 5(2), pages 149-156, 1996. MML Identifier: FILTER_2
    Summary: The dual concept to filters (see \cite{FILTER_0.ABS}, \cite{FILTER_1.ABS}) i.e. ideals of a lattice is introduced.
  51. Grzegorz Bancerek. Categorial Categories and Slice Categories, Formalized Mathematics 5(2), pages 157-165, 1996. MML Identifier: CAT_5
    Summary: By categorial categories we mean categories with categories as objects and morphisms of the form $(C_1, C_2, F)$, where $C_1$ and $C_2$ are categories and $F$ is a functor from $C_1$ into $C_2$.
  52. Grzegorz Bancerek. Subtrees, Formalized Mathematics 5(2), pages 185-190, 1996. MML Identifier: TREES_9
    Summary: The concepts of root tree, the set of successors of a node in decorated tree and sets of subtrees are introduced.
  53. Grzegorz Bancerek. Terms Over Many Sorted Universal Algebra, Formalized Mathematics 5(2), pages 191-198, 1996. MML Identifier: MSATERM
    Summary: Pure terms (without constants) over a signature of many sorted universal algebra and terms with constants from algebra are introduced. Facts on evaluation of a term in some valuation are proved.
  54. Yatsuka Nakamura, Grzegorz Bancerek. Combining of Circuits, Formalized Mathematics 5(2), pages 283-295, 1996. MML Identifier: CIRCCOMB
    Summary: We continue the formalisation of circuits started in \cite{PRE_CIRC.ABS},\cite{MSAFREE2.ABS},\cite{CIRCUIT1.ABS}, \cite{CIRCUIT2.ABS}. Our goal was to work out the notation of combining circuits which could be employed to prove the properties of real circuits.
  55. Grzegorz Bancerek. Indexed Category, Formalized Mathematics 5(3), pages 329-337, 1996. MML Identifier: INDEX_1
    Summary: The concept of indexing of a category (a part of indexed category, see \cite{TarleckiBurstallGoguen}) is introduced as a pair formed by a many sorted category and a many sorted functor. The indexing of a category $C$ against to \cite{TarleckiBurstallGoguen} is not a functor but it can be treated as a functor from $C$ into some categorial category (see \cite{CAT_5.ABS}). The goal of the article is to work out the notation necessary to define institutions (see \cite{GoguenBurstall}).
  56. Grzegorz Bancerek, Yatsuka Nakamura. Full Adder Circuit. Part I, Formalized Mathematics 5(3), pages 367-380, 1996. MML Identifier: FACIRC_1
    Summary: We continue the formalisation of circuits started by Piotr Rudnicki, Andrzej Trybulec, Pauline Kawamoto, and the second author in \cite{PRE_CIRC.ABS}, \cite{MSAFREE2.ABS}, \cite{CIRCUIT1.ABS}, \cite{CIRCUIT2.ABS}. The first step in proving properties of full $n$-bit adder circuit, i.e. 1-bit adder, is presented. We employ the notation of combining circuits introduced in \cite{CIRCCOMB.ABS}.
  57. Grzegorz Bancerek. Continuous, Stable, and Linear Maps of Coherence Spaces, Formalized Mathematics 5(3), pages 381-393, 1996. MML Identifier: COHSP_1
    Summary:
  58. Grzegorz Bancerek. Minimal Signature for Partial Algebra, Formalized Mathematics 5(3), pages 405-414, 1996. MML Identifier: PUA2MSS1
    Summary: The concept of characterizing of partial algebras by many sorted signature is introduced, i.e. we say that a signature $S$ characterizes a partial algebra $A$ if there is an $S$-algebra whose sorts form a partition of the carrier of algebra $A$ and operations are formed from operations of $A$ by the partition. The main result is that for any partial algebra there is the minimal many sorted signature which characterizes the algebra. The minimality means that there are signature endomorphisms from any signature which characterizes the algebra $A$ onto the minimal one.
  59. Grzegorz Bancerek. Reduction Relations, Formalized Mathematics 5(4), pages 469-478, 1996. MML Identifier: REWRITE1
    Summary: The goal of the article is to start the formalization of Knuth-Bendix completion method (see \cite{BachmairDershowitz}, \cite{KlopMiddeldorp} or \cite{HofLinCS}; see also \cite{KnuthBendix},\cite{Huet81}), i.e. to formalize the concept of the completion of a reduction relation. The completion of a reduction relation $R$ is a complete reduction relation equivalent to $R$ such that convertible elements have the same normal forms. The theory formalized in the article includes concepts and facts concerning normal forms, terminating reductions, Church-Rosser property, and equivalence of reduction relations.
  60. Grzegorz Bancerek, Andrzej Trybulec. Miscellaneous Facts about Functions, Formalized Mathematics 5(4), pages 485-492, 1996. MML Identifier: FUNCT_7
    Summary:
  61. Grzegorz Bancerek. Translations, Endomorphisms, and Stable Equational Theories, Formalized Mathematics 5(4), pages 553-564, 1996. MML Identifier: MSUALG_6
    Summary: Equational theories of an algebra, i.e. the equivalence relation closed under translations and endomorphisms, are formalized. The correspondence between equational theories and term rewriting systems is discussed in the paper. We get as the main result that any pair of elements of an algebra belongs to the equational theory generated by a set $A$ of axioms iff the elements are convertible w.r.t. term rewriting reduction determined by $A$.\par The theory is developed according to \cite{WECHLER}.
  62. Grzegorz Bancerek. Bounds in Posets and Relational Substructures, Formalized Mathematics 6(1), pages 81-91, 1997. MML Identifier: YELLOW_0
    Summary: Notation and facts necessary to start with the formalization of continuous lattices according to \cite{CCL} are introduced.
  63. Grzegorz Bancerek. Directed Sets, Nets, Ideals, Filters, and Maps, Formalized Mathematics 6(1), pages 93-107, 1997. MML Identifier: WAYBEL_0
    Summary: Notation and facts necessary to start with the formalization of continuous lattices according to \cite{CCL} are introduced. The article contains among other things, the definition of directed and filtered subsets of a poset (see 1.1 in \cite[p.~2]{CCL}), the definition of nets on the poset (see 1.2 in \cite[p.~2]{CCL}), the definition of ideals and filters and the definition of maps preserving arbitrary and directed sups and arbitrary and filtered infs (1.9 also in \cite[p.~4]{CCL}). The concepts of semilattices, sup-semiletices and poset lattices (1.8 in \cite[p.~4]{CCL}) are also introduced. A number of facts concerning the above notion and including remarks 1.4, 1.5, and 1.10 from \cite[pp.~3--5]{CCL} is presented.
  64. Grzegorz Bancerek. The ``Way-Below'' Relation, Formalized Mathematics 6(1), pages 169-176, 1997. MML Identifier: WAYBEL_3
    Summary: In the paper the ``way-below" relation, in symbols $x \ll y$, is introduced. Some authors prefer the term ``relatively compact" or ``way inside", since in the poset of open sets of a topology it is natural to read $U \ll V$ as ``$U$ is relatively compact in $V$". A compact element of a poset (or an element isolated from below) is defined to be way below itself. So, the compactness in the poset of open sets of a topology is equivalent to the compactness in that topology.\par The article includes definitions, facts and examples 1.1--1.8 presented in \cite[pp.~38--42]{CCL}.
  65. Grzegorz Bancerek. Duality in Relation Structures, Formalized Mathematics 6(2), pages 227-232, 1997. MML Identifier: YELLOW_7
    Summary:
  66. Grzegorz Bancerek. Prime Ideals and Filters, Formalized Mathematics 6(2), pages 241-247, 1997. MML Identifier: WAYBEL_7
    Summary: The part of \cite[pp.~73--77]{CCL}, i.e. definitions and propositions 3.16--3.27, is formalized in the paper.
  67. Grzegorz Bancerek. Institution of Many Sorted Algebras. Part I: Signature Reduct of an Algebra, Formalized Mathematics 6(2), pages 279-287, 1997. MML Identifier: INSTALG1
    Summary: In the paper the notation necessary to construct the institution of many sorted algebras is introduced.
  68. Grzegorz Bancerek. Closure Operators and Subalgebras, Formalized Mathematics 6(2), pages 295-301, 1997. MML Identifier: WAYBEL10
    Summary:
  69. Grzegorz Bancerek. Algebra of Morphisms, Formalized Mathematics 6(2), pages 303-310, 1997. MML Identifier: CATALG_1
    Summary:
  70. Grzegorz Bancerek. Bases and Refinements of Topologies, Formalized Mathematics 7(1), pages 35-43, 1998. MML Identifier: YELLOW_9
    Summary:
  71. Grzegorz Bancerek. The Lawson Topology, Formalized Mathematics 7(2), pages 163-168, 1998. MML Identifier: WAYBEL19
    Summary: The article includes definitions, lemmas and theorems 1.1--1.7, 1.9, 1.10 presented in Chapter III of \cite[pp.~142--146]{CCL}.
  72. Grzegorz Bancerek. Lawson Topology in Continuous Lattices, Formalized Mathematics 7(2), pages 177-184, 1998. MML Identifier: WAYBEL21
    Summary: The article completes Mizar formalization of Section 1 of Chapter III of \cite[pp.~145--147]{CCL}.
  73. Grzegorz Bancerek. Retracts and Inheritance, Formalized Mathematics 9(1), pages 77-85, 2001. MML Identifier: YELLOW16
    Summary:
  74. Grzegorz Bancerek. Technical Preliminaries to Algebraic Specifications, Formalized Mathematics 9(1), pages 87-93, 2001. MML Identifier: ALGSPEC1
    Summary:
  75. Grzegorz Bancerek. Continuous Lattices of Maps between T$_0$ Spaces, Formalized Mathematics 9(1), pages 111-117, 2001. MML Identifier: WAYBEL26
    Summary: Formalization of \cite[pp. 128--130]{CCL}, chapter II, section 4 (4.1 -- 4.9).
  76. Grzegorz Bancerek, Adam Naumowicz. Function Spaces in the Category of Directed Suprema Preserving Maps, Formalized Mathematics 9(1), pages 171-177, 2001. MML Identifier: WAYBEL27
    Summary: Formalization of \cite[pp. 115--117]{ccl}, chapter II, section 2 (2.5 -- 2.10).
  77. Grzegorz Bancerek, Adam Naumowicz. The Characterization of the Continuity of Topologies, Formalized Mathematics 9(2), pages 241-247, 2001. MML Identifier: WAYBEL29
    Summary: Formalization of \cite[pp. 128--130]{CCL}, chapter II, section 4 (4.10, 4.11).
  78. Grzegorz Bancerek. Concrete Categories, Formalized Mathematics 9(3), pages 605-621, 2001. MML Identifier: YELLOW18
    Summary: In the paper, we develop the notation of duality and equivalence of categories and concrete categories based on \cite{ALTCAT_1.ABS}. The development was motivated by the duality theory for continuous lattices (see \cite[p. 189]{CCL}), where we need to cope with concrete categories of lattices and maps preserving their properties. For example, the category {\it UPS} of complete lattices and directed suprema preserving maps; or the category {\it INF} of complete lattices and infima preserving maps. As the main result of this paper it is shown that every category is isomorphic to its concretization (the concrete category with the same objects). Some useful schemes to construct categories and functors are also presented.
  79. Grzegorz Bancerek. Circuit Generated by Terms and Circuit Calculating Terms, Formalized Mathematics 9(3), pages 645-657, 2001. MML Identifier: CIRCTRM1
    Summary: In the paper we investigate the dependence between the structure of circuits and sets of terms. Circuits in our terminology (see \cite{CIRCUIT1.ABS}) are treated as locally-finite many sorted algebras over special signatures. Such approach enables to formalize every real circuit. The goal of this investigation is to specify circuits by terms and, enentualy, to have methods of formal verification of real circuits. The following notation is introduced in this paper: \begin{itemize} \item structural equivalence of circuits, i.e. equivalence of many sorted signatures, \item embedding of a circuit into another one, \item similarity of circuits (a concept narrower than isomorphism of many sorted algebras over equivalent signatures), \item calculation of terms by a circuit according to an algebra, \item specification of circuits by terms and an algebra. \end{itemize}
  80. Grzegorz Bancerek, Piotr Rudnicki. The Set of Primitive Recursive Functions, Formalized Mathematics 9(4), pages 705-720, 2001. MML Identifier: COMPUT_1
    Summary: We follow \cite{Uspenski60} in defining the set of primitive recursive functions. The important helper notion is the homogeneous function from finite sequences of natural numbers into natural numbers where homogeneous means that all the sequences in the domain are of the same length. The set of all such functions is then used to define the notion of a set closed under composition of functions and under primitive recursion. We call a set primitively recursively closed iff it contains the initial functions (nullary constant function returning 0, unary successor and projection functions for all arities) and is closed under composition and primitive recursion. The set of primitive recursive functions is then defined as the smallest set of functions which is primitive recursively closed. We show that this set can be obtained by primitive recursive approximation. We finish with showing that some simple and well known functions are primitive recursive.
  81. Grzegorz Bancerek, Noboru Endou, Yuji Sakai. On the Characterizations of Compactness, Formalized Mathematics 9(4), pages 733-738, 2001. MML Identifier: YELLOW19
    Summary: In the paper we show equivalence of the convergence of filters on a topological space and the convergence of nets in the space. We also give, five characterizations of compactness. Namely, for any topological space $T$ we proved that following condition are equivalent: \begin{itemize} \itemsep-3pt \item $T$ is compact, \item every ultrafilter on $T$ is convergent, \item every proper filter on $T$ has cluster point, \item every net in $T$ has cluster point, \item every net in $T$ has convergent subnet, \item every Cauchy net in $T$ is convergent. \end{itemize}
  82. Grzegorz Bancerek, Noboru Endou. Compactness of Lim-inf Topology, Formalized Mathematics 9(4), pages 739-743, 2001. MML Identifier: WAYBEL33
    Summary: Formalization of \cite{CCL}, chapter III, section 3 (3.4--3.6).
  83. Grzegorz Bancerek. Miscellaneous Facts about Functors, Formalized Mathematics 9(4), pages 745-754, 2001. MML Identifier: YELLOW20
    Summary: In the paper we show useful facts concerning reverse and inclusion functors and the restriction of functors. We also introduce a new notation for the intersection of categories and the isomorphism under arbitrary functors.
  84. Grzegorz Bancerek. Categorial Background for Duality Theory, Formalized Mathematics 9(4), pages 755-765, 2001. MML Identifier: YELLOW21
    Summary: In the paper, we develop the notation of lattice-wise categories as concrete categories (see \cite{YELLOW18.ABS}) of lattices. Namely, the categories based on \cite{ALTCAT_1.ABS} with lattices as objects and at least monotone maps between them as morphisms. As examples, we introduce the categories {\it UPS}, {\it CONT}, and {\it ALG} with complete, continuous, and algebraic lattices, respectively, as objects and directed suprema preserving maps as morphisms. Some useful schemes to construct categories of lattices and functors between them are also presented.
  85. Grzegorz Bancerek. Duality Based on the Galois Connection. Part I, Formalized Mathematics 9(4), pages 767-778, 2001. MML Identifier: WAYBEL34
    Summary: In the paper, we investigate the duality of categories of complete lattices and maps preserving suprema or infima according to \cite[p. 179--183; 1.1--1.12]{CCL}. The duality is based on the concept of the Galois connection.
  86. Grzegorz Bancerek, Artur Kornilowicz. Yet Another Construction of Free Algebra, Formalized Mathematics 9(4), pages 779-785, 2001. MML Identifier: MSAFREE3
    Summary:
  87. Tetsuya Tsunetou, Grzegorz Bancerek, Yatsuka Nakamura. Zero-Based Finite Sequences, Formalized Mathematics 9(4), pages 825-829, 2001. MML Identifier: AFINSQ_1
    Summary:
  88. Hisayoshi Kunimune, Grzegorz Bancerek, Yatsuka Nakamura. On State Machines of Calculating Type, Formalized Mathematics 9(4), pages 857-864, 2001. MML Identifier: FSM_2
    Summary: In this article, we show the properties of the calculating type state machines. In the first section, we have defined calculating type state machines of which the state transition only depends on the first input. We have also proved theorems of the state machines. In the second section, we defined Moore machines with final states. We also introduced the concept of result of the Moore machines. In the last section, we proved the correctness of several calculating type of Moore machines.
  89. Grzegorz Bancerek, Shin'nosuke Yamaguchi, Yasunari Shidama. Combining of Multi Cell Circuits, Formalized Mathematics 10(1), pages 47-64, 2002. MML Identifier: CIRCCMB2
    Summary: In this article we continue the investigations from \cite{CIRCCOMB.ABS} and \cite{FACIRC_1.ABS} of verification of a circuit design. We concentrate on the combination of multi cell circuits from given cells (circuit modules). Namely, we formalize a design of the form \\ \input CIRCCMB2.PIC and prove its stability. The formalization proposed consists in a series of schemes which allow to define multi cells circuits and prove their properties. Our goal is to achive mathematical formalization which will allow to verify designs of real circuits.
  90. Grzegorz Bancerek, Shin'nosuke Yamaguchi, Katsumi Wasaki. Full Adder Circuit. Part II, Formalized Mathematics 10(1), pages 65-71, 2002. MML Identifier: FACIRC_2
    Summary: In this article we continue the investigations from \cite{FACIRC_1.ABS} of verification of a design of adder circuit. We define it as a combination of 1-bit adders using schemes from \cite{CIRCCMB2.ABS}. $n$-bit adder circuit has the following structure\\ \input FACIRC_2.PIC As the main result we prove the stability of the circuit. Further works will consist of the proof of full correctness of the circuit.
  91. Grzegorz Bancerek, Adam Naumowicz. Preliminaries to Automatic Generation of Mizar Documentation for Circuits, Formalized Mathematics 10(3), pages 117-133, 2002. MML Identifier: CIRCCMB3
    Summary: In this paper we introduce technical notions used by a system which automatically generates Mizar documentation for specified circuits. They provide a ready for use elements needed to justify correctness of circuits' construction. We concentrate on the concept of stabilization and analyze one-gate circuits and their combinations.
  92. Grzegorz Bancerek, Mitsuru Aoki, Akio Matsumoto, Yasunari Shidama. Processes in Petri nets, Formalized Mathematics 11(1), pages 125-132, 2003. MML Identifier: PNPROC_1
    Summary: Sequential and concurrent compositions of processes in Petri nets are introduced. A process is formalized as a set of (possible), so called, firing sequences. In the definition of the sequential composition the standard concatenation is used $$ R_1 \mathop{\rm before} R_2 = \{p_1\mathop{^\frown}p_2: p_1\in R_1\ \land\ p_2\in R_2\} $$ The definition of the concurrent composition is more complicated $$ R_1 \mathop{\rm concur} R_2 = \{ q_1\cup q_2: q_1\ {\rm misses}\ q_2\ \land\ \mathop{\rm Seq} q_1\in R_1\ \land\ \mathop{\rm Seq} q_2\in R_2\} $$ For example, $$ \{\langle t_0\rangle\} \mathop{\rm concur} \{\langle t_1,t_2\rangle\} = \{\langle t_0,t_1,t_2\rangle , \langle t_1,t_0,t_2\rangle , \langle t_1,t_2,t_0\rangle\} $$ The basic properties of the compositions are shown.
  93. Shin'nosuke Yamaguchi, Grzegorz Bancerek, Katsumi Wasaki. Full Subtracter Circuit. Part II, Formalized Mathematics 11(3), pages 231-236, 2003. MML Identifier: FSCIRC_2
    Summary: In this article we continue investigations from \cite{FSCIRC_1.ABS} of verification of a design of subtracter circuit. We define it as a combination of multi cell circuit using schemes from \cite{CIRCCMB2.ABS}. As the main result we prove the stability of the circuit.
  94. Grzegorz Bancerek. On Semilattice Structure of Mizar Types, Formalized Mathematics 11(4), pages 355-369, 2003. MML Identifier: ABCMIZ_0
    Summary: The aim of this paper is to develop a formal theory of Mizar types. The presented theory is an approach to the structure of Mizar types as a sup-semilattice with widening (subtyping) relation as the order. It is an abstraction from the existing implementation of the Mizar verifier and formalization of the ideas from \cite{Bancerek:2003}.
  95. Takashi Mitsuishi, Grzegorz Bancerek. Lattice of Fuzzy Sets, Formalized Mathematics 11(4), pages 393-398, 2003. MML Identifier: LFUZZY_0
    Summary: This article concerns a connection of fuzzy logic and lattice theory. Namely, the fuzzy sets form a Heyting lattice with union and intersection of fuzzy sets as meet and join operations. The lattice of fuzzy sets is defined as the product of interval posets. As the final result, we have characterized the composition of fuzzy relations in terms of lattice theory and proved its associativity.
  96. Takashi Mitsuishi, Grzegorz Bancerek. Transitive Closure of Fuzzy Relations, Formalized Mathematics 12(1), pages 15-20, 2004. MML Identifier: LFUZZY_1
    Summary:
  97. Gijs Geleijnse, Grzegorz Bancerek. Properties of Groups, Formalized Mathematics 12(3), pages 347-350, 2004. MML Identifier: GROUP_8
    Summary: In this article we formalize theorems from Chapter 1 of \cite{Hall:1959}. Our article covers Theorems 1.5.4, 1.5.5 (inequality on indices), 1.5.6 (equality of indices), Lemma 1.6.1 and several other supporting theorems needed to complete the formalization.
  98. Grzegorz Bancerek. On the Characteristic and Weight of a Topological Space, Formalized Mathematics 13(1), pages 163-169, 2005. MML Identifier: TOPGEN_2
    Summary: We continue Mizar formalization of General Topology according to the book \cite{ENGEL:1} by Engelking. In the article the formalization of Section 1.1 is completed. Namely, the paper includes the formalization of theorems on correspondence of the basis and basis in a point, definitions of the character of a point and a topological space, a neighborhood system, and the weight of a topological space. The formalization is tested with almost discrete topological spaces with infinity.
  99. Grzegorz Bancerek. On Constructing Topological Spaces and Sorgenfrey Line, Formalized Mathematics 13(1), pages 171-179, 2005. MML Identifier: TOPGEN_3
    Summary: We continue Mizar formalization of General Topology according to the book \cite{ENGEL:1} by Engelking. In the article the formalization of Section 1.2 is almost completed. Namely, we formalize theorems on introduction of topologies by bases, neighborhood systems, closed sets, closure operator, and interior operator. The Sorgenfrey line is defined by a basis. It is proved that the weight of it is continuum. Other techniques are used to demonstrate introduction of discrete and anti-discrete topologies.
  100. Artur Kornilowicz, Grzegorz Bancerek, Adam Naumowicz. Tietze Extension Theorem, Formalized Mathematics 13(4), pages 471-475, 2005. MML Identifier: TIETZE
    Summary: In this paper we formalize the Tietze extension theorem using as a basis the proof presented at the PlanetMath web server (\url{http://planetmath.org/encyclopedia/ProofOfTietzeExtensionTheorem2.html}).
  101. Adam Naumowicz, Grzegorz Bancerek. Homeomorphisms of Jordan Curves, Formalized Mathematics 13(4), pages 477-480, 2005. MML Identifier: JORDAN24
    Summary: In this paper we prove that simple closed curves can be homeomorphically framed into a given rectangle. We also show that homeomorphisms preserve the Jordan property.
  102. Grzegorz Bancerek. Niemytzki Plane - an Example of Tychonoff Space Which Is Not $T_4$, Formalized Mathematics 13(4), pages 515-524, 2005. MML Identifier: TOPGEN_5
    Summary: We continue Mizar formalization of General Topology according to the book \cite{ENGEL:1} by Engelking. Niemytzki plane is defined as halfplane $y \geq 0$ with topology introduced by a neighborhood system. Niemytzki plane is not $T_4$. Next, the definition of Tychonoff space is given. The characterization of Tychonoff space by prebasis and the fact that Tychonoff spaces are between $T_3$ and $T_4$ is proved. The final result is that Niemytzki plane is also a Tychonoff space.
Jozef Bialas
  1. Jozef Bialas. Group and Field Definitions, Formalized Mathematics 1(3), pages 433-439, 1990. MML Identifier: REALSET1
    Summary: The article contains exactly the same definitions of group and field as those in \cite{DIEUDONNE}. These definitions were prepared without the help of the definitions and properties of {\it Nat} and {\it Real} modes included in the MML. This is the first of a series of articles in which we are going to introduce the concept of the set of real numbers in a elementary axiomatic way.
  2. Jozef Bialas. Properties of Fields, Formalized Mathematics 1(5), pages 807-812, 1990. MML Identifier: REALSET2
    Summary: The second part of considerations concerning groups and fields. It includes a definition and properties of commutative field $F$ as a structure defined by: the set, a support of $F$, containing two different elements, by two binary operations ${\bf +}_{F}$, ${\bf \cdot}_{F}$ on this set, called addition and multiplication, and by two elements from the support of $F$, ${\bf 0}_{F}$ being neutral for addition and ${\bf 1}_{F}$ being neutral for multiplication. This structure is named a field if $\langle$the support of $F$, ${\bf +}_{F}$, ${\bf 0}_{F} \rangle$ and $\langle$the support of $F$, ${\bf \cdot}_{F}$, ${\bf 1}_{F} \rangle$ are commutative groups and multiplication has the property of left-hand and right-hand distributivity with respect to addition. It is demonstrated that the field $F$ satisfies the definition of a field in the axiomatic approach.
  3. Jozef Bialas. Several Properties of Fields. Field Theory, Formalized Mathematics 2(1), pages 159-162, 1991. MML Identifier: REALSET3
    Summary: The article includes a continuation of the paper \cite{REALSET2.ABS}. Some simple theorems concerning basic properties of a field are proved.
  4. Jozef Bialas. Infimum and Supremum of the Set of Real Numbers. Measure Theory, Formalized Mathematics 2(1), pages 163-171, 1991. MML Identifier: SUPINF_1
    Summary: We introduce some properties of the least upper bound and the greatest lower bound of the subdomain of $\overline{\Bbb R}$ numbers, where $\overline{\Bbb R}$ denotes the enlarged set of real numbers, $\overline{\Bbb R} = {\Bbb R} \cup \{-\infty,+\infty\}$. The paper contains definitions of majorant and minorant elements, bounded from above, bounded from below and bounded sets, sup and inf of set, for nonempty subset of $\overline{\Bbb R}$. We prove theorems describing the basic relationships among those definitions. The work is the first part of the series of articles concerning the Lebesgue measure theory.
  5. Jozef Bialas. Series of Positive Real Numbers. Measure Theory, Formalized Mathematics 2(1), pages 173-183, 1991. MML Identifier: SUPINF_2
    Summary: We introduce properties of a series of nonnegative $\overline{\Bbb R}$ numbers, where $\overline{\Bbb R}$ denotes the enlarged set of real numbers, $\overline{\Bbb R} = {\Bbb R} \cup \{-\infty,+\infty\}$. The paper contains definition of sup $F$ and inf $F$, for $F$ being function, and a definition of a sumable subset of $\overline{\Bbb R}$. We proved the basic theorems regarding the definitions mentioned above. The work is the second part of a series of articles concerning the Lebesgue measure theory.
  6. Jozef Bialas. The $\sigma$-additive Measure Theory, Formalized Mathematics 2(2), pages 263-270, 1991. MML Identifier: MEASURE1
    Summary: The article contains definition and basic properties of $\sigma$-additive, nonnegative 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}. We present definitions of $\sigma$-field of sets, $\sigma$-additive measure, measurable sets, measure zero sets and the basic theorems describing relationships between the notion mentioned above. The work is the third part of the series of articles concerning the Lebesgue measure theory.
  7. Jozef Bialas. Several Properties of the $\sigma$-additive Measure, Formalized Mathematics 2(4), pages 493-497, 1991. MML Identifier: MEASURE2
    Summary: A continuation of \cite{MEASURE1.ABS}. The paper contains the definition and basic properties of a $\sigma$-additive, nonnegative 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 R.~Sikorski \cite{SIKORSKI:1}. Some simple theorems concerning basic properties of a $\sigma$-additive measure, measurable sets, measure zero sets are proved. The work is the fourth part of the series of articles concerning the Lebesgue measure theory.
  8. Jozef Bialas. Completeness of the $\sigma$-Additive Measure. Measure Theory, Formalized Mathematics 2(5), pages 689-693, 1991. MML Identifier: MEASURE3
    Summary: Definitions and basic properties of a $\sigma$-additive, non-negative 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{MEASURE2.ABS}. Some theorems concerning basic properties of a $\sigma$-additive measure and completeness of the measure are proved.
  9. 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\-dor's 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}. Caratheodor's theorem and some theorems concerning basic properties of Caratheodor's measure are proved. The work is the sixth part of the series of articles concerning the Lebesgue measure theory.
  10. 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.
  11. Jozef Bialas. Some Properties of the Intervals, Formalized Mathematics 5(1), pages 21-26, 1996. MML Identifier: MEASURE6
    Summary:
  12. Jozef Bialas. The One-Dimensional Lebesgue Measure, Formalized Mathematics 5(2), pages 253-258, 1996. MML Identifier: MEASURE7
    Summary: The paper is the crowning of a series of articles written in the Mizar language, being a formalization of notions needed for the description of the one-dimensional Lebesgue measure. The formalization of the notion as classical as the Lebesgue measure determines the powers of the PC Mizar system as a tool for the strict, precise notation and verification of the correctness of deductive theories. Following the successive articles \cite{SUPINF_1.ABS}, \cite{SUPINF_2.ABS}, \cite{MEASURE1.ABS}, \cite{MEASURE6.ABS} constructed so that the final one should include the definition and the basic properties of the Lebesgue measure, we observe one of the paths relatively simple in the sense of the definition, enabling us the formal introduction of this notion. This way, although toilsome, since such is the nature of formal theories, is greatly instructive. It brings home the proper succession of the introduction of the definitions of intermediate notions and points out to those elements of the theory which determine the essence of the complexity of the notion being introduced.\par The paper includes the definition of the $\sigma$-field of Lebesgue measurable sets, the definition of the Lebesgue measure and the basic set of the theorems describing its properties.
  13. Jozef Bialas, Yatsuka Nakamura. The Theorem of Weierstrass, Formalized Mathematics 5(3), pages 353-359, 1996. MML Identifier: WEIERSTR
    Summary:
  14. Jozef Bialas, Yatsuka Nakamura. Dyadic Numbers and T$_4$ Topological Spaces, Formalized Mathematics 5(3), pages 361-366, 1996. MML Identifier: URYSOHN1
    Summary:
  15. Jozef Bialas, Yatsuka Nakamura. Some Properties of Dyadic Numbers and Intervals, Formalized Mathematics 9(3), pages 627-630, 2001. MML Identifier: URYSOHN2
    Summary: The article is the second part of a paper proving the fundamental Urysohn Theorem concerning the existence of a real valued continuous function on a normal topological space. The paper is divided into two parts. In the first part, we introduce some definitions and theorems concerning properties of intervals; in the second we prove some of properties of dyadic numbers used in proving Urysohn Lemma.
  16. Jozef Bialas, Yatsuka Nakamura. The Urysohn Lemma, Formalized Mathematics 9(3), pages 631-636, 2001. MML Identifier: URYSOHN3
    Summary: This article is the third part of a paper proving the fundamental Urysohn Theorem concerning the existence of a real valued continuous function on a normal topological space. The paper is divided into two parts. In the first part, we describe the construction of the function solving thesis of the Urysohn Lemma. The second part contains the proof of the Urysohn Lemma in normal space and the proof of the same theorem for compact space.
Slawomir Bialecki
  1. Bogdan Nowak, Slawomir Bialecki. Zermelo's Theorem, Formalized Mathematics 1(3), pages 431-432, 1990. MML Identifier: WELLSET1
    Summary: The article contains direct proof of Zermelo's theorem about the existence of a well ordering for any set and the lemma the proof depends on.
Leszek Borys
  1. Leszek Borys. Paracompact and Metrizable Spaces, Formalized Mathematics 2(4), pages 481-485, 1991. MML Identifier: PCOMPS_1
    Summary: We give an example of a compact space. Next we define a locally finite subset family of a topological space and a paracompact topological space. An open sets family of a metric space we define next and it has been shown that the metric space with any open sets family is a topological space. Next we define metrizable space.
  2. 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}).
Patrick Braselmann
  1. Patrick Braselmann, Peter Koepke. Substitution in First-Order Formulas: Elementary Properties, Formalized Mathematics 13(1), pages 5-15, 2005. MML Identifier: SUBSTUT1
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"o}del's famous completeness theorem (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349-360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article introduces the basic concepts of substitution of a variable for a variable in a first-order formula. The contents of this article correspond to Chapter III par. 8, Definition 8.1, 8.2 of Ebbinghaus, Flum, Thomas.
  2. Patrick Braselmann, Peter Koepke. Coincidence Lemma and Substitution Lemma, Formalized Mathematics 13(1), pages 17-26, 2005. MML Identifier: SUBLEMMA
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"o}del's famous completeness theorem (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349--360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article establishes further concepts of substitution of a variable for a variable in a first-order formula. The main result is the substitution lemma. The contents of this article correspond to Chapter III par. 5, 5.1 Coincidence Lemma and Chapter III par. 8, 8.3 Substitution Lemma of Ebbinghaus, Flum, Thomas.
  3. Patrick Braselmann, Peter Koepke. Substitution in First-Order Formulas. Part II. The Construction of First-Order Formulas, Formalized Mathematics 13(1), pages 27-32, 2005. MML Identifier: SUBSTUT2
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"o}del's famous completeness theorem (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349-360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article establishes that every substitution can be applied to every formula as in Chapter III par. 8, Definition 8.1, 8.2 of Ebbinghaus, Flum, Thomas. After that, it is observed that substitution doesn't change the number of quantifiers of a formula. Then further details about substitution and some results about the construction of formulas are proven.
  4. Patrick Braselmann, Peter Koepke. A Sequent Calculus for First-Order Logic, Formalized Mathematics 13(1), pages 33-39, 2005. MML Identifier: CALCUL_1
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"o}del's famous completeness theorem (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349--360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article introduces a sequent calculus for first-order logic. The correctness of this calculus is shown and some important inferences are derived. The contents of this article correspond to Chapter IV of Ebbinghaus, Flum, Thomas.
  5. Patrick Braselmann, Peter Koepke. Consequences of the Sequent Calculus, Formalized Mathematics 13(1), pages 41-44, 2005. MML Identifier: CALCUL_2
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"{o}}del's famous completeness theorem (K. G{\"{o}}del, ``Die Vollst{\"{a}}ndigkeit der Axiome des logischen Funktionenkalk{\"{u}}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349-360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The first main result of the present article is that the derivablility of a sequent doesn't depend on the ordering of the antecedent. The second main result says: if a sequent is derivable, then the formulas in the antecendent only need to occur once.
  6. Patrick Braselmann, Peter Koepke. Equivalences of Inconsistency and Henkin Models, Formalized Mathematics 13(1), pages 45-48, 2005. MML Identifier: HENMODEL
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"{o}}del's famous completeness theorem (K. G{\"{o}}del, ``Die Vollst{\"{a}}ndigkeit der Axiome des logischen Funktionenkalk{\"{u}}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349--360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag, New York Inc. The present article establishes some equivalences of inconsistency. It is proved that a countable union of consistent sets is consistent. Then the concept of a Henkin model is introduced. The contents of this article correspond to Chapter IV, par. 7 and Chapter V, par. 1 of Ebbinghaus, Flum, Thomas.
  7. Patrick Braselmann, Peter Koepke. G\"odel's Completeness Theorem, Formalized Mathematics 13(1), pages 49-53, 2005. MML Identifier: GOEDELCP
    Summary: This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt G{\"o}del's famous completeness theorem (K. G{\"o}del, ``Die Vollst{\"a}ndigkeit der Axiome des logischen Funktionenkalk{\"u}ls'', Monatshefte f\"ur Mathematik und Physik 37 (1930), 349--360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article contains the proof of a simplified completeness theorem for a countable relational language without equality.
Ewa Burakowska
  1. Ewa Burakowska, Beata Madras. Real Function One-Side Differentiability, Formalized Mathematics 2(5), pages 653-656, 1991. MML Identifier: FDIFF_3
    Summary: We define real function one-side differentiability and one-side continuity. Main properties of one-side differentiability function are proved. Connections between one-side differential and differential real function at the point are demonstrated.
  2. Ewa Burakowska. Subalgebras of the Universal Algebra. Lattices of Subalgebras, Formalized Mathematics 4(1), pages 23-27, 1993. MML Identifier: UNIALG_2
    Summary: Introduces a definition of a subalgebra of a universal algebra. A notion of similar algebras and basic operations on subalgebras such as a subalgebra generated by a set, the intersection and the sum of two subalgebras were introduced. Some basic facts concerning the above notions have been proved. The article also contains the definition of a lattice of subalgebras of a universal algebra.
  3. Ewa Burakowska. Subalgebras of Many Sorted Algebra. Lattice of Subalgebras, Formalized Mathematics 5(1), pages 47-54, 1996. MML Identifier: MSUALG_2
    Summary:
Czeslaw Bylinski
  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. Czeslaw Bylinski. Partial Functions, Formalized Mathematics 1(2), pages 357-367, 1990. MML Identifier: PARTFUN1
    Summary: In the article we define partial functions. We also define the following notions related to partial functions and functions themselves: the empty function, the restriction of a function to a partial function from a set into a set, the set of all partial functions from a set into a set, the total functions, the relation of tolerance of two functions and the set of all total functions which are tolerated by a partial function. Some simple propositions related to the introduced notions are proved. In the beginning of this article we prove some auxiliary theorems and schemes related to the articles: \cite{FUNCT_1.ABS} and \cite{FUNCT_2.ABS}.
  8. Czeslaw Bylinski. Introduction to Categories and Functors, Formalized Mathematics 1(2), pages 409-420, 1990. MML Identifier: CAT_1
    Summary: The category is introduced as an ordered 5-tuple of the form $\langle O, M, dom, cod, \cdot, id \rangle$ where $O$ (objects) and $M$ (morphisms) are arbitrary nonempty sets, $dom$ and $cod$ map $M$ onto $O$ and assign to a morphism domain and codomain, $\cdot$ is a partial binary map from $M \times M$ to $M$ (composition of morphisms), $id$ applied to an object yields the identity morphism. We define the basic notions of the category theory such as hom, monic, epi, invertible. We next define functors, the composition of functors, faithfulness and fullness of functors, isomorphism between categories and the identity functor.
  9. Andrzej Trybulec, Czeslaw Bylinski. Some Properties of Real Numbers, Formalized Mathematics 1(3), pages 445-449, 1990. MML Identifier: SQUARE_1
    Summary: We define the following operations on real numbers: $max(x,y)$, $min(x,y)$, $x^2$, $\sqrt{x}$. We prove basic properties of introduced operations. A number of auxiliary theorems absent in \cite{REAL_1.ABS} and \cite{ABSVALUE.ABS} is proved.
  10. Czeslaw Bylinski, Grzegorz Bancerek. Variables in Formulae of the First Order Language, Formalized Mathematics 1(3), pages 459-469, 1990. MML Identifier: QC_LANG3
    Summary: We develop the first order language defined in \cite{QC_LANG1.ABS}. We continue the work done in the article \cite{QC_LANG2.ABS}. We prove some schemes of defining by structural induction. We deal with notions of closed subformulae and of still not bound variables in a formula. We introduce the concept of the set of all free variables and the set of all fixed variables occurring in a formula.
  11. Czeslaw Bylinski. The Complex Numbers, Formalized Mathematics 1(3), pages 507-513, 1990. MML Identifier: COMPLEX1
    Summary: We define the set $\Bbb C$ of complex numbers as the set of all ordered pairs $z =\langle a,b\rangle$ where $a$ and $b$ are real numbers and where addition and multiplication are defined. We define the real and imaginary parts of $z$ and denote this by $a = \Re(z)$, $b = \Im(z)$. These definitions satisfy all the axioms for a field. $0_{\Bbb C} = 0+0i$ and $1_{\Bbb C} = 1+0i$ are identities for addition and multiplication respectively, and there are multiplicative inverses for each non zero element in $\Bbb C$. The difference and division of complex numbers are also defined. We do not interpret the set of all real numbers $\Bbb R$ as a subset of $\Bbb C$. From here on we do not abandon the ordered pair notation for complex numbers. For example: $i^2 = (0+1i)^2 = -1+0i \neq -1$. We conclude this article by introducing two operations on $\Bbb C$ which are not field operations. We define the absolute value of $z$ denoted by $|z|$ and the conjugate of $z$ denoted by $z^\ast$.
  12. Czeslaw Bylinski. The Modification of a Function by a Function and the Iteration of the Composition of a Function, Formalized Mathematics 1(3), pages 521-527, 1990. MML Identifier: FUNCT_4
    Summary: In the article we introduce some operations on functions. We define the natural ordering relation on functions. The fact that a function $f$ is less than a function $g$ we denote by $f \leq g$ and we define by $\hbox{graph} f \subseteq \hbox{graph} f$. In the sequel we define the modifications of a function $f$ by a function $g$ denoted $f \hbox{+$\cdot$} g$ and the $n$-th iteration of the composition of a function $f$ denoted by $f^n$. We prove some propositions related to the introduced notions.
  13. Czeslaw Bylinski. Finite Sequences and Tuples of Elements of a Non-empty Sets, Formalized Mathematics 1(3), pages 529-536, 1990. MML Identifier: FINSEQ_2
    Summary: The first part of the article is a continuation of \cite{FINSEQ_1.ABS}. Next, we define the identity sequence of natural numbers and the constant sequences. The main part of this article is the definition of tuples. The element of a set of all sequences of the length $n$ of $D$ is called a tuple of a non-empty set $D$ and it is denoted by element of $D^{n}$. Also some basic facts about tuples of a non-empty set are proved.
  14. Czeslaw Bylinski. Binary Operations Applied to Finite Sequences, Formalized Mathematics 1(4), pages 643-649, 1990. MML Identifier: FINSEQOP
    Summary: The article contains some propositions and theorems related to \cite{FUNCOP_1.ABS} and \cite{FINSEQ_2.ABS}. The notions introduced in \cite{FUNCOP_1.ABS} are extended to finite sequences. A number of additional propositions related to this notions are proved. There are also proved some properties of distributive operations and unary operations. The notation and propositions for inverses are introduced.
  15. Czeslaw Bylinski. Semigroup operations on finite subsets, Formalized Mathematics 1(4), pages 651-656, 1990. MML Identifier: SETWOP_2
    Summary: A continuation of \cite{SETWISEO.ABS}. The propositions and theorems proved in \cite{SETWISEO.ABS} are extended to finite sequences. Several additional theorems related to semigroup operations of functions not included in \cite{SETWISEO.ABS} are proved. The special notation for operations on finite sequences is introduced.
  16. Czeslaw Bylinski. The Sum and Product of Finite Sequences of Real Numbers, Formalized Mathematics 1(4), pages 661-668, 1990. MML Identifier: RVSUM_1
    Summary: Some operations on the set of $n$-tuples of real numbers are introduced. Addition, difference of such $n$-tuples, complement of a $n$-tuple and multiplication of these by real numbers are defined. In these definitions more general properties of binary operations applied to finite sequences from \cite{FINSEQOP.ABS} are used. Then the fact that certain properties are satisfied by those operations is demonstrated directly from \cite{FINSEQOP.ABS}. Moreover some properties can be recognized as being those of real vector space. Multiplication of $n$-tuples of real numbers and square power of $n$-tuple of real numbers using for notation of some properties of finite sums and products of real numbers are defined, followed by definitions of the finite sum and product of $n$-tuples of real numbers using notions and properties introduced in \cite{SETWOP_2.ABS}. A number of propositions and theorems on sum and product of finite sequences of real numbers are proved. As additional properties there are proved some properties of real numbers and set representations of binary operations on real numbers.
  17. Czeslaw Bylinski. A Classical First Order Language, Formalized Mathematics 1(4), pages 669-676, 1990. MML Identifier: CQC_LANG
    Summary: The aim is to construct a language for the classical predicate calculus. The language is defined as a subset of the language constructed in \cite{QC_LANG1.ABS}. Well-formed formulas of this language are defined and some usual connectives and quantifiers of \cite{QC_LANG1.ABS}, \cite{QC_LANG2.ABS} are accordingly. We prove inductive and definitional schemes for formulas of our language. Substitution for individual variables in formulas of the introduced language is defined. This definition is borrowed from \cite{POGORZELSKI.1975}. For such purpose some auxiliary notation and propositions are introduced.
  18. Czeslaw Bylinski. Subcategories and Products of Categories, Formalized Mathematics 1(4), pages 725-732, 1990. MML Identifier: CAT_2
    Summary: The {\it subcategory} of a category and product of categories is defined. The {\it inclusion functor} is the injection (inclusion) map $E \atop \hookrightarrow$ which sends each object and each arrow of a Subcategory $E$ of a category $C$ to itself (in $C$). The inclusion functor is faithful. {\it Full subcategories} of $C$, that is, those subcategories $E$ of $C$ such that $\hbox{Hom}_E(a,b) = \hbox{Hom}_C(b,b)$ for any objects $a,b$ of $E$, are defined. A subcategory $E$ of $C$ is full when the inclusion functor $E \atop \hookrightarrow$ is full. The proposition that a full subcategory is determined by giving the set of objects of a category is proved. The product of two categories $B$ and $C$ is constructed in the usual way. Moreover, some simple facts on $bifunctors$ (functors from a product category) are proved. The final notions in this article are that of projection functors and product of two functors ({\it complex} functors and {\it product} functors).
  19. Czeslaw Bylinski, Andrzej Trybulec. Complex Spaces, Formalized Mathematics 2(1), pages 151-158, 1991. MML Identifier: COMPLSP1
    Summary: We introduce the concept of $n$-dimensional complex space. We prove a number of simple but useful propositions concerning addition, nultiplication by scalars and similar basic concepts. We introduce metric and topology. We prove that $n$-dimensional complex space is a Hausdorff space and that it is regular.
  20. Czeslaw Bylinski. Opposite Categories and Contravariant Functors, Formalized Mathematics 2(3), pages 419-424, 1991. MML Identifier: OPPCAT_1
    Summary: The opposite category of a category, contravariant functors and duality functors are defined.
  21. Czeslaw Bylinski. Category Ens, Formalized Mathematics 2(4), pages 527-533, 1991. MML Identifier: ENS_1
    Summary: If $V$ is any non-empty set of sets, we define $\hbox{\bf Ens}_V$ to be the category with the objects of all sets $X \in V$, morphisms of all mappings from $X$ into $Y$, with the usual composition of mappings. By a mapping we mean a triple $\langle X,Y,f \rangle$ where $f$ is a function from $X$ into $Y$. The notations and concepts included corresponds to that presented in \cite{SEMAD}, \cite{MacLane:1}. We also introduce representable functors to illustrate properties of the category {\bf Ens}.
  22. Czeslaw Bylinski. Products and Coproducts in Categories, Formalized Mathematics 2(5), pages 701-709, 1991. MML Identifier: CAT_3
    Summary: A product and coproduct in categories are introduced. The concepts included correspond to that presented in \cite{SEMAD}.
  23. 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)$.
  24. Yatsuka Nakamura, Czeslaw Bylinski. Extremal Properties of Vertices on Special Polygons. Part I, Formalized Mathematics 5(1), pages 97-102, 1996. MML Identifier: SPPOL_1
    Summary: First, extremal properties of endpoints of line segments in n-dimensional Euclidean space are discussed. Some topological properties of line segments are also discussed. Secondly, extremal properties of vertices of special polygons which consist of horizontal and vertical line segments in 2-dimensional Euclidean space, are also derived.
  25. Czeslaw Bylinski. Some Properties of Restrictions of Finite Sequences, Formalized Mathematics 5(2), pages 241-245, 1996. MML Identifier: FINSEQ_5
    Summary: The aim of the paper is to define some basic notions of restrictions of finite sequences.
  26. Czeslaw Bylinski, Yatsuka Nakamura. Special Polygons, Formalized Mathematics 5(2), pages 247-252, 1996. MML Identifier: SPPOL_2
    Summary:
  27. Czeslaw Bylinski, Piotr Rudnicki. The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. Part I, Formalized Mathematics 5(4), pages 577-582, 1996. MML Identifier: MSSCYC_1
    Summary: We prove a number of auxiliary facts about graphs, mainly about vertex sequences of chains and oriented chains. Then we define a graph to be {\em well-founded} if for each vertex in the graph the length of oriented chains ending at the vertex is bounded. A {\em well-founded} graph does not have directed cycles or infinite descending chains. In the second part of the article we prove some auxiliary facts about free algebras and locally-finite algebras.
  28. Czeslaw Bylinski, Piotr Rudnicki. The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. Part II, Formalized Mathematics 5(4), pages 591-593, 1996. MML Identifier: MSSCYC_2
    Summary: The graph induced by a many sorted signature is defined as follows: the vertices are the symbols of sorts, and if a sort $s$ is an argument of an operation with result sort $t$, then a directed edge $[s, t]$ is in the graph. The key lemma states relationship between the depth of elements of a free many sorted algebra over a signature and the length of directed chains in the graph induced by the signature. Then we prove that a monotonic many sorted signature (every finitely-generated algebra over it is locally-finite) induces a {\em well-founded} graph. The converse holds with an additional assumption that the signature is finitely operated, i.e. there is only a finite number of operations with the given result sort.
  29. Mariusz Zynel, Czeslaw Bylinski. Properties of Relational Structures, Posets, Lattices and Maps, Formalized Mathematics 6(1), pages 123-130, 1997. MML Identifier: YELLOW_2
    Summary: In the paper we present some auxiliary facts concerning posets and maps between them. Our main purpose, however is to give an account on complete lattices and lattices of ideals. A sufficient condition that a lattice might be complete, the fixed-point theorem and two remarks upon images of complete lattices in monotone maps, introduced in \cite[pp. 8--9]{CCL}, can be found in Section~7. Section~8 deals with lattices of ideals. We examine the meet and join of two ideals. In order to show that the lattice of ideals is complete, the infinite intersection of ideals is investigated.
  30. Czeslaw Bylinski. Galois Connections, Formalized Mathematics 6(1), pages 131-143, 1997. MML Identifier: WAYBEL_1
    Summary: The paper is the Mizar encoding of the chapter 0 section 3 of \cite{CCL} In the paper the following concept are defined: Galois connections, Heyting algebras, and Boolean algebras.
  31. 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.
  32. 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.
  33. Yatsuka Nakamura, Andrzej Trybulec, Czeslaw Bylinski. Bounded Domains and Unbounded Domains, Formalized Mathematics 8(1), pages 1-13, 1999. MML Identifier: JORDAN2C
    Summary: First, notions of inside components and outside components are introduced for any subset of $n$-dimensional Euclid space. Next, notions of the bounded domain and the unbounded domain are defined using the above components. If the dimension is larger than 1, and if a subset is bounded, a unbounded domain of the subset coincides with an outside component (which is unique) of the subset. For a sphere in $n$-dimensional space, the similar fact is true for a bounded domain. In 2 dimensional space, any rectangle also has such property. We discussed relations between the Jordan property and the concept of boundary, which are necessary to find points in domains near a curve. In the last part, we gave the sufficient criterion for belonging to the left component of some clockwise oriented finite sequences.
  34. Czeslaw Bylinski. Gauges, Formalized Mathematics 8(1), pages 25-27, 1999. MML Identifier: JORDAN8
    Summary:
  35. Czeslaw Bylinski. Some Properties of Cells on Go-Board, Formalized Mathematics 8(1), pages 139-146, 1999. MML Identifier: GOBRD13
    Summary:
  36. Czeslaw Bylinski, Mariusz Zynel. Cages -- the External Approximation of Jordan's Curve, Formalized Mathematics 9(1), pages 19-24, 2001. MML Identifier: JORDAN9
    Summary: On the Euclidean plane Jordan's curve may be approximated with a polygonal path of sides parallel to coordinate axes, either externally, or internally. The paper deals with the external approximation, and the existence of a {\em Cage} -- an external polygonal path -- is proved.
  37. Czeslaw Bylinski. Introduction to Real Linear Topological Spaces, Formalized Mathematics 13(1), pages 99-107, 2005. MML Identifier: RLTOPSP1
    Summary:
Jianbing Cao
  1. Fahui Zhai, Jianbing Cao, Xiquan Liang. Circled Sets, Circled Hull, and Circled Family, Formalized Mathematics 13(4), pages 447-451, 2005. MML Identifier: CIRCLED1
    Summary: In this article, we prove some basic properties of the circled sets. We also define the circled hull, and give the definition of circled family.
  2. Jianbing Cao, Fahui Zhai, Xiquan Liang. Partial Sum and Partial Product of Some Series, Formalized Mathematics 13(4), pages 501-503, 2005. MML Identifier: SERIES_4
    Summary: This article contains partial sum and partial product of some series which are often used.
  3. Jianbing Cao, Fahui Zhai, Xiquan Liang. Some Differentiable Formulas of Special Functions, Formalized Mathematics 13(4), pages 505-509, 2005. MML Identifier: FDIFF_5
    Summary: This article contains some differentiable formulas of special functions.
Patricia L. Carlson
  1. Patricia L. Carlson, Grzegorz Bancerek. Context-Free Grammar -- Part 1, Formalized Mathematics 2(5), pages 683-687, 1991. MML Identifier: LANG1
    Summary: The concept of context-free grammar and of derivability in grammar are introduced. Moreover, the language (set of finite sequences of symbols) generated by grammar and some grammars are defined. The notion convenient to prove facts on language generated by grammar with exchange of symbols on grammar of union and concatenation of languages is included.
Pacharapokin Chanapat
  1. Pacharapokin Chanapat, Kanchun,, Hiroshi Yamazaki. Formulas and Identities of Trigonometric Functions, Formalized Mathematics 12(2), pages 139-141, 2004. MML Identifier: SIN_COS4
    Summary: In this article, we concentrated especially on addition formulas of fundamental trigonometric functions, and their identities.
  2. Pacharapokin Chanapat, Hiroshi Yamazaki. Formulas and Identities of Hyperbolic Functions, Formalized Mathematics 13(4), pages 511-513, 2005. MML Identifier: SIN_COS8
    Summary: In this article, we proved formulas of hyperbolic sine, hyperbolic cosine and hyperbolic tangent, and their identities.
Wenpai Chang
  1. Wenpai Chang, Yatsuka Nakamura, Piotr Rudnicki. Inner Products and Angles of Complex Numbers, Formalized Mathematics 11(3), pages 275-280, 2003. MML Identifier: COMPLEX2
    Summary: An inner product of complex numbers is defined and used to characterize the (counter-clockwise) angle between ($a$,0) and (0,$b$) in the complex plane. For complex $a$, $b$ and $c$ we then define the (counter-clockwise) angle between ($a$,$c$) and ($c$, $b$) and prove theorems about the sum of internal and external angles of a triangle.
  2. Wenpai Chang, Hiroshi Yamazaki, Yatsuka Nakamura. A Theory of Matrices of Complex Elements, Formalized Mathematics 13(1), pages 157-162, 2005. MML Identifier: MATRIX_5
    Summary: A concept of ``Matrix of Complex'' is defined here. Addition, subtraction, scalar multiplication and product are introduced using correspondent definitions of ``Matrix of Field''. Many equations for such operations consist of a case of ``Matrix of Field''. A calculation method of product of matrices is shown using a finite sequence of Complex in the last theorem.
  3. Wenpai Chang, Hiroshi Yamazaki, Yatsuka Nakamura. The Inner Product and Conjugate of Finite Sequences of Complex Numbers, Formalized Mathematics 13(3), pages 367-373, 2005. MML Identifier: COMPLSP2
    Summary: A concept of "the inner product and conjugate of finite sequences of complex numbers" is defined here. Addition, subtraction, Scalar multiplication and inner product are introduced using correspondent definitions of "conjugate of finite sequences of Field". Many equations for such operations consist like a case of "conjugate of finite sequences of Field". Some operations on the set of $n$-tuples of complex numbers are introduced as well. Addition, difference of such $n$-tuples, complement of a $n$-tuple and multiplication of these are defined in terms of complex numbers.
  4. Wenpai Chang, Hiroshi Yamazaki, Yatsuka Nakamura. The Inner Product and Conjugate of Matrix of Complex Numbers, Formalized Mathematics 13(4), pages 493-499, 2005. MML Identifier: MATRIXC1
    Summary: Concepts of the inner product and conjugate of matrix of complex numbers are defined here. Operations such as addition, subtraction, scalar multiplication and inner product are introduced using correspondent definitions of the conjugate of a matrix of a complex field. Many equations for such operations consist like a case of the conjugate of matrix of a field and some operations on the set of sum of complex numbers are introduced.
  5. Yatsuka Nakamura, Nobuyuki Tamura, Wenpai Chang. A Theory of Matrices of Real Elements, Formalized Mathematics 14(1), pages 21-28, 2006. MML Identifier: MATRIXR1
    Summary: Here, the concept of matrix of real elements is introduced. This is defined as a special case of the general concept of matrix of a field. For such a real matrix, the notions of addition, subtraction, scalar product are defined. For any real finite sequences, two transformations to matrices are introduced. One of the matrices is of width 1, and the other is of length 1. By such transformations, two products of a matrix and a finite sequence are defined. The linearity of such product is shown.
Jing-Chao Chen
  1. 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.
  2. Jing-Chao Chen. While M