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: 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.