Formalized Mathematics    (ISSN 1426-2630)
Volume 6, Number 2 (1997): pdf, ps, dvi.
  1. Adam Grabowski. Auxiliary and Approximating Relations, Formalized Mathematics 6(2), pages 179-188, 1997. MML Identifier: WAYBEL_4
    Summary: The aim of this paper is to formalize the second part of Chapter I Section 1 (1.9--1.19) in \cite{CCL}. Definitions of Scott's auxiliary and approximating relations are introduced in this work. We showed that in a meet-continuous lattice, the way-below relation is the intersection of all approximating auxiliary relations (proposition (40) --- compare 1.13 in \cite[pp.~43--47]{CCL}). By (41) a continuous lattice is a complete lattice in which $\ll$ is the smallest approximating auxiliary relation. The notions of the strong interpolation property and the interpolation property are also introduced.
  2. Katsumi Wasaki, Pauline N. Kawamoto. 2's Complement Circuit, Formalized Mathematics 6(2), pages 189-197, 1997. MML Identifier: TWOSCOMP
    Summary: This article introduces various Boolean operators which are used in discussing the properties and stability of a 2's complement circuit. We present the definitions and related theorems for the following logical operators which include negative input/output: 'and2a', 'or2a', 'xor2a' and 'nand2a', 'nor2a', etc. We formalize the concept of a 2's complement circuit, define the structures of complementors/incrementors for binary operations, and prove the stability of the circuit.
  3. Mariusz Zynel. The Equational Characterization of Continuous Lattices, Formalized Mathematics 6(2), pages 199-205, 1997. MML Identifier: WAYBEL_5
    Summary: The class of continuous lattices can be characterized by infinitary equations. Therefore, it is closed under the formation of subalgebras and homomorphic images. Following the terminology of \cite{Johnstone} we introduce a continuous lattice subframe to be a sublattice closed under the formation of arbitrary infs and directed sups. This notion corresponds with a subalgebra of a continuous lattice in \cite{CCL}.\par The class of completely distributive lattices is also introduced in the paper. Such lattices are complete and satisfy the most restrictive type of the general distributivity law. Obviously each completely distributive lattice is a Heyting algebra. It was hard to find the best Mizar implementation of the complete distributivity equational condition (denoted by CD in \cite{CCL}). The powerful and well developed Many Sorted Theory gives the most convenient way of this formalization. A set double indexed by $K$, introduced in the paper, corresponds with a family $\{x_{j,k}: j\in J, k\in K(j)\}$. It is defined to be a suitable many sorted function. Two special functors: $\rm Sups$ and $\rm Infs$ as counterparts of $\rm Sup$ and $\rm Inf$ respectively, introduced in \cite{YELLOW_2.ABS}, are also defined. Originally the equation in Definition~2.4 of \cite[p.~58]{CCL} looks as follows: $${\textstyle\bigwedge}_{j\in J} {\textstyle\bigvee}_{k\in K(j)} x_{j,k} = {\textstyle\bigvee}_{f\in M} {\textstyle\bigwedge}_{j\in J} x_{j,f(j)},$$ where $M$ is the set of functions defined on $J$ with values $f(j)\in K(j)$.
  4. Agnieszka Julia Marasik. Miscellaneous Facts about Relation Structure, Formalized Mathematics 6(2), pages 207-211, 1997. MML Identifier: YELLOW_5
    Summary: In the article notation and facts necessary to start with formalization of continuous lattices according to \cite{CCL} are introduced.
  5. Andrzej Trybulec. Moore-Smith Convergence, Formalized Mathematics 6(2), pages 213-225, 1997. MML Identifier: YELLOW_6
    Summary: The paper introduces the concept of a net (a generalized sequence). The goal is to enable the continuation of the translation of \cite{CCL}.
  6. Grzegorz Bancerek. Duality in Relation Structures, Formalized Mathematics 6(2), pages 227-232, 1997. MML Identifier: YELLOW_7
    Summary:
  7. Beata Madras. Irreducible and Prime Elements, Formalized Mathematics 6(2), pages 233-239, 1997. MML Identifier: WAYBEL_6
    Summary: In the paper open and order generating subsets are defined. Irreducible and prime elements are also defined. The article includes definitions and facts presented in \cite[pp.~68--72]{CCL}.
  8. 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.
  9. Robert Milewski. Algebraic Lattices, Formalized Mathematics 6(2), pages 249-254, 1997. MML Identifier: WAYBEL_8
    Summary:
  10. Yatsuka Nakamura, Roman Matuszewski. Reconstructions of Special Sequences, Formalized Mathematics 6(2), pages 255-263, 1997. MML Identifier: JORDAN3
    Summary: We discuss here some methods for reconstructing special sequences which generate special polygonal arcs in ${\cal E}^{2}_{\rm T}$. For such reconstructions we introduce a ``mid" function which cuts out the middle part of a sequence; the ``$\downharpoonleft$" function, which cuts down the left part of a sequence at some point; the ``$\downharpoonright$" function for cutting down the right part at some point; and the ``$\downharpoonleft \downharpoonright$" function for cutting down both sides at two given points.\par We also introduce some methods glueing two special sequences. By such cutting and glueing methods, the speciality of sequences (generatability of special polygonal arcs) is shown to be preserved.
  11. Adam Naumowicz. Conjugate Sequences, Bounded Complex Sequences and Convergent Complex Sequences, Formalized Mathematics 6(2), pages 265-268, 1997. MML Identifier: COMSEQ_2
    Summary: This article is a continuation of \cite{COMSEQ_1.ABS}. It is divided into five sections. The first one contains a few useful lemmas. In the second part there is a definition of conjugate sequences and proofs of some basic properties of such sequences. The third segment treats of bounded complex sequences,next one contains description of convergent complex sequences. The last and the biggest part of the article contains proofs of main theorems concerning the theory of bounded and convergent complex sequences.
  12. Artur Kornilowicz. On the Topological Properties of Meet-Continuous Lattices, Formalized Mathematics 6(2), pages 269-277, 1997. MML Identifier: WAYBEL_9
    Summary: This work is continuation of formalization of \cite{CCL}. Proposition 4.4 from Chapter 0 is proved.
  13. 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.
  14. Andrzej Trybulec. Baire Spaces, Sober Spaces, Formalized Mathematics 6(2), pages 289-294, 1997. MML Identifier: YELLOW_8
    Summary: In the article concepts and facts necessary to continue formalization of theory of continuous lattices according to \cite{CCL} are introduced.
  15. Grzegorz Bancerek. Closure Operators and Subalgebras, Formalized Mathematics 6(2), pages 295-301, 1997. MML Identifier: WAYBEL10
    Summary:
  16. Grzegorz Bancerek. Algebra of Morphisms, Formalized Mathematics 6(2), pages 303-310, 1997. MML Identifier: CATALG_1
    Summary:
  17. Andrzej Trybulec. Scott Topology, Formalized Mathematics 6(2), pages 311-319, 1997. MML Identifier: WAYBEL11
    Summary: In the article we continue the formalization in Mizar of \cite[98--105]{CCL}. We work with structures of the form $$L = \langle C,\ \leq,\ \tau \rangle,$$ where $C$ is the carrier of the structure, $\leq$ - an ordering relation on $C$ and $\tau$ a family of subsets of $C$. When $\langle C,\ \leq \rangle$ is a complete lattice we say that $L$ is Scott, if $\tau$ is the Scott topology of $\langle C,\ \leq \rangle$. We define the Scott convergence (lim inf convergence). Following \cite{CCL} we prove that in the case of a continuous lattice $\langle C,\ \leq \rangle$ the Scott convergence is topological, i.e. enjoys the properties: (CONSTANTS), (SUBNETS), (DIVERGENCE), (ITERATED LIMITS). We formalize the theorem, that if the Scott convergence has the (ITERATED LIMITS) property, the $\langle C,\ \leq \rangle$ is continuous.
  18. Artur Kornilowicz. On the Baire Category Theorem, Formalized Mathematics 6(2), pages 321-327, 1997. MML Identifier: WAYBEL12
    Summary: In this paper Exercise 3.43 from Chapter 1 of \cite{CCL} is solved.