Formalized Mathematics    ISSN 1898-9934 (e), ISSN 1426-2630 (p)

Volume 14, Number 2 (2006): PDF A copy of this issue can also be found on the MetaPress server (with DOI names of articles).

  1. Marco Riccardi. Pocklington's Theorem and Bertrand's Postulate, Formalized Mathematics 14(2), pages 47-52, 2006. MML Identifier: NAT_4
    Summary: The first four sections include some auxiliary theorems related to number and finite sequence of numbers, in particular a primality test, the Pocklington's theorem (see \cite{LeVeque}). The last section presents the formalization of Bertrand's postulate closely following the book \cite{PFTB}, pp. 7--9.
  2. Noboru Endou, Yasunari Shidama. Integral of Measurable Function, Formalized Mathematics 14(2), pages 53-70, 2006. MML Identifier: MESFUNC5
    Summary: In this paper we construct integral of measurable function.