@MISC{DUALSP05.MIZ,
  AUTHOR = {Narita, Keiko and Nakasho, Kazuhisa and Shidama, Yasunari},
  TITLE = {F. Riesz Theorem},
  SECTION1 = {The Normed Space of Continuous Functions on Closed Interval},
  SECTION2 = {Preliminaries},
  SECTION3 = {F. Riesz Theorem},
  DAY = {30},
  MONTH = {August},
  YEAR = {2017},
  ADDRESS1 = {Hirosaki-city, Aomori, Japan},
  ADDRESS2 = {Akita Prefectural University\\Akita},
  ADDRESS3 = {Shinshu University\\Nagano},
  MSC2010 = {46E15 46B10},
  KEYWORDS = {F. Riesz theorem; dual spaces; continuous functions},
  SUMMARY = {In this article, we described F. Riesz theorem.
  In the first section, we defined
  Mizar functor \verb!ClstoCmp!, compact topological spaces as closed interval subset of real numbers.
  Then using the former definition and referring to the article \cite{C0SP1.ABS} and the article
  \cite{C0SP2.ABS}, we defined the normed spaces of continuous functions on closed interval
  subset of real numbers, and defined the normed spaces of bounded functions on closed
  interval subset of real numbers. We also proved some related properties.
  In Sec.2, we proved some lemmas for the proof of F. Riesz theorem.
  In Sec.3, we proved F. Riesz theorem, about the dual space of the space of continuous
  functions on closed interval subset of real numbers, finally.
  We applied Hahn-Banach theorem \cite{DUALSP01.ABS:36} to the proof of the last theorem.
  For the description of theorems of this section, we also referred to the article
  \cite{INTEGR22.ABS} and the article\cite{INTEGR23.ABS}.
  These formalizations are based on \cite{Brezis2011}, \cite{Dax2002}, \cite{Rudin1991}, and
  \cite{Yoshida1980}.}}

@BOOK{Brezis2011,
  TITLE = {Functional Analysis, Sobolev Spaces and Partial Differential Equations}
  AUTHOR = {Haim Brezis},
  PUBLISHER = {Springer}
  YEAR = {2011},
}
@BOOK{Dax2002,
  TITLE = {Functional Analysis. Pure and Applied Mathematics: A Wiley Series of
Texts, Monographs and Tracts},
  AUTHOR = {Peter D. Dax},
  PUBLISHER = {Wiley Interscience},
  YEAR = {2002},
}
@BOOK{Rudin1991,
  TITLE = {Functional Analysis},
  AUTHOR = {Walter Rudin},
  PUBLISHER = {New York, McGraw-Hill},
  YEAR = {1991}
  EDITION = {2nd}
}
@BOOK{Yoshida1980,
  TITLE = {Functional Analysis},
  AUTHOR = {Kosaku Yoshida},
  PUBLISHER = {Springer}
  YEAR = {1980},
}
