Formalization of Orthogonal Complements of Normed Spaces

In this study we are formalizing the optimization theory in Mizar. It is well known that geometric principles of linear vector space theory play fundamental roles in optimization. This article focuses on formalization of definitions and some theorems about dual spaces: we formalize orthogonal complements of real normed spaces, then we deal with minimum norm problems.