Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

**Noboru Endou**- Gifu National College of Technology
**Takashi Mitsuishi**- Miyagi University
**Yasunari Shidama**- Shinshu University, Nagano

- Convexity is one of the most important concepts in a study of analysis. Especially, it has been applied around the optimization problem widely. Our purpose is to define the concept of convexity of a set on Mizar, and to develop the generalities of convex analysis. The construction of this article is as follows: Convexity of the set is defined in the section 1. The section 2 gives the definition of convex combination which is a kind of the linear combination and related theorems are proved there. In section 3, we define the convex hull which is an intersection of all convex sets including a given set. The last section is some theorems which are necessary to compose this article.

- Convex Sets
- Convex Combinations
- Convex Hull
- Miscellaneous

- [1]
Grzegorz Bancerek.
Cardinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Czeslaw Bylinski.
The sum and product of finite sequences of real numbers.
*Journal of Formalized Mathematics*, 2, 1990. - [6]
Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama.
Dimension of real unitary space.
*Journal of Formalized Mathematics*, 14, 2002. - [7]
Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama.
Topology of real unitary space.
*Journal of Formalized Mathematics*, 14, 2002. - [8]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [9]
Beata Padlewska and Agata Darmochwal.
Topological spaces and continuous functions.
*Journal of Formalized Mathematics*, 1, 1989. - [10]
Jan Popiolek.
Introduction to Banach and Hilbert spaces --- part I.
*Journal of Formalized Mathematics*, 3, 1991. - [11]
Andrzej Trybulec.
Enumerated sets.
*Journal of Formalized Mathematics*, 1, 1989. - [12]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [13]
Andrzej Trybulec.
Subsets of real numbers.
*Journal of Formalized Mathematics*, Addenda, 2003. - [14]
Wojciech A. Trybulec.
Subspaces and cosets of subspaces in real linear space.
*Journal of Formalized Mathematics*, 1, 1989. - [15]
Wojciech A. Trybulec.
Vectors in real linear space.
*Journal of Formalized Mathematics*, 1, 1989. - [16]
Wojciech A. Trybulec.
Linear combinations in real linear space.
*Journal of Formalized Mathematics*, 2, 1990. - [17]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]