Formalized Mathematics    (ISSN 1898-9934 (Online), ISSN 1426-2630 (Print))
Volume 11, Number 4 (2003): pdf, ps, dvi.
  1. Andrzej Trybulec. On the Sets Inhabited by Numbers, Formalized Mathematics 11(4), pages 341-347, 2003. MML Identifier: MEMBERED
    Summary: The information that all members of a set enjoy a property expressed by an adjective can be processed in a systematic way. The purpose of the work is to find out how to do that. If it works, `membered' will become a reserved word and the work with it will be automated. I have chosen {\it membered} rather than {\it inhabited} because of the compatibility with the Automath terminology. The phrase $\tau$ {\it inhabits} $\theta$ could be translated to $\tau$ {\bfseries\itshape is} $\theta$ in Mizar.
  2. Grigory E. Ivanov. Definition of Convex Function and Jensen's Inequality, Formalized Mathematics 11(4), pages 349-354, 2003. MML Identifier: CONVFUN1
    Summary: Convexity of a function in a real linear space is defined as convexity of its epigraph according to ``Convex analysis'' by R. Tyrrell Rockafellar. The epigraph of a function is a subset of the product of the function's domain space and the space of real numbers. Therefore the product of two real linear spaces should be defined. The values of the functions under consideration are extended real numbers. We define the sum of a finite sequence of extended real numbers and get some properties of the sum. The relation between notions ``function is convex'' and ``function is convex on set'' (see RFUNCT\_3:def 13) is established. We obtain another version of the criterion for a set to be convex (see CONVEX2:6 to compare) that may be more suitable in some cases. Finally we prove Jensen's inequality (both strict and not strict) as criteria for functions to be convex.
  3. 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}.
  4. Akihiro Kubo. Lines in $n$-Dimensional Euclidean Spaces, Formalized Mathematics 11(4), pages 371-376, 2003. MML Identifier: EUCLID_4
    Summary: In this paper, we define the line of $n$-dimensional Euclidian space and we introduce basic properties of affine space on this space. Next, we define the inner product of elements of this space. At the end, we introduce orthogonality of lines of this space.
  5. Yasumasa Suzuki, Noboru Endou, Yasunari Shidama. Banach Space of Absolute Summable Real Sequences, Formalized Mathematics 11(4), pages 377-380, 2003. MML Identifier: RSSPACE3
    Summary: A continuation of \cite{RSSPACE2.ABS}. As the example of real norm spaces, we introduce the arithmetic addition and multiplication in the set of absolute summable real sequences and introduce the norm also. This set has the structure of the Banach space.
  6. 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.
  7. Yatsuka Nakamura, Hiroshi Yamazaki. Calculation of Matrices of Field Elements. Part I, Formalized Mathematics 11(4), pages 385-391, 2003. MML Identifier: MATRIX_4
    Summary: This article gives property of calculation of matrices.
  8. 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.
  9. Adam Grabowski. On the Kuratowski Limit Operators, Formalized Mathematics 11(4), pages 399-409, 2003. MML Identifier: KURATO_2
    Summary: In the paper we give formal descriptions of the two Kuratowski limit oprators: Li $S$ and Ls $S$, where $S$ is an arbitrary sequence of subsets of a fixed topological space. In the two last sections we prove basic properties of these lower and upper topological limits, which may be found e.g. in \cite{KURAT:2}. In the sections 2--4, we present three operators which are associated in some sense with the above mentioned, that is lim inf $F$, lim sup $F$, and limes $F$, where $F$ is a sequence of subsets of a fixed 1-sorted structure.
  10. Andrzej Trybulec. On the Segmentation of a Simple Closed Curve, Formalized Mathematics 11(4), pages 411-416, 2003. MML Identifier: JORDAN_A
    Summary: The main goal of the work was to introduce the concept of the segmentation of a simple closed curve into (arbitrary small) arcs. The existence of it has been proved by Yatsuka Nakamura \cite{JORDAN7.ABS}. The concept of the gap of a segmentation is also introduced. It is the smallest distance between disjoint segments in the segmentation. For this purpose, the relationship between segments of an arc \cite{JORDAN6.ABS} and segments on a simple closed curve \cite{JORDAN7.ABS} has been shown.
  11. Shunichi Kobayashi. On the Calculus of Binary Arithmetics, Formalized Mathematics 11(4), pages 417-419, 2003. MML Identifier: BINARI_5
    Summary: In this paper, we have binary arithmetic and its related operations. We include some theorems concerning logical operators.
  12. Artur Kornilowicz, Yasunari Shidama. SCMPDS Is Not Standard, Formalized Mathematics 11(4), pages 421-424, 2003. MML Identifier: SCMPDS_9
    Summary: The aim of the paper is to show that SCMPDS (\cite{SCMPDS_2.ABS}) does not belong to the class of standard computers (\cite{AMISTD_1.ABS}).
  13. Robert Milewski. On the Upper and Lower Approximations of the Curve, Formalized Mathematics 11(4), pages 425-430, 2003. MML Identifier: JORDAN19
    Summary: