Convex Sets and Convex Combinations

Abstract

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.