• the hol light theory of euclidean space

    نویسندگان :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 939
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     we describe the library of theorems about n-dimensional euclidean space that has been formalized in the hol light prover. this formalization was started in 2005 and has been extensively developed since then, partly in direct support of the flyspeck project, partly out of a general desire to develop a well-rounded and comprehensive theory of basic analytical, geometrical and topological machinery. the library includes various ‘big name’ theorems (brouwer’s fixed point theorem, the stone-weierstrass theorem, the tietze extension theorem), numerous non-trivial results that are useful in applications (second mean value theorem for integrals, power series for real and complex transcendental functions) and a host of supporting definitions and lemmas. it also includes some specialized automated proof tools. the library has as planned been applied to the flyspeck project and has become the basis of a significant development of results in complex analysis, among others.

سوال خود را در مورد این مقاله مطرح نمایید :

با انتخاب دکمه ثبت پرسش، موافقت خود را با قوانین انتشار محتوا در وبسایت تی پی بین اعلام می کنم