Cousin’s Lemma

• Autorzy: Roland Coghetto
• Języki publikacji: EN

Abstrakty

EN

We formalize, in two different ways, that “the n-dimensional Euclidean metric space is a complete metric space” (version 1. with the results obtained in [13], [26], [25] and version 2., the results obtained in [13], [14], (registrations) [24]). With the Cantor’s theorem - in complete metric space (proof by Karol Pąk in [22]), we formalize “The Nested Intervals Theorem in 1-dimensional Euclidean metric space”. Pierre Cousin’s proof in 1892 [18] the lemma, published in 1895 [9] states that: “Soit, sur le plan YOX, une aire connexe S limitée par un contour fermé simple ou complexe; on suppose qu’à chaque point de S ou de son périmètre correspond un cercle, de rayon non nul, ayant ce point pour centre : il est alors toujours possible de subdiviser S en régions, en nombre fini et assez petites pour que chacune d’elles soit complétement intérieure au cercle correspondant à un point convenablement choisi dans S ou sur son périmètre.” (In the plane YOX let S be a connected area bounded by a closed contour, simple or complex; one supposes that at each point of S or its perimeter there is a circle, of non-zero radius, having this point as its centre; it is then always possible to subdivide S into regions, finite in number and sufficiently small for each one of them to be entirely inside a circle corresponding to a suitably chosen point in S or on its perimeter) [23]. Cousin’s Lemma, used in Henstock and Kurzweil integral [29] (generalized Riemann integral), state that: “for any gauge δ, there exists at least one δ-fine tagged partition”. In the last section, we formalize this theorem. We use the suggestions given to the Cousin’s Theorem p.11 in [5] and with notations: [4], [29], [19], [28] and [12].

Słowa kluczowe

EN

Cousin’s lemma; Cousin’s theorem; nested intervals theorem

Kategorie tematyczne

• 03B35: Mechanization of proofs and logical operations
• 54D30: Compactness

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2016
• Tom: 24
• Numer: 2
• Strony: 107-119

Daty

wydano

2016-06-01

otrzymano

2015-12-31

online

2016-12-08

Twórcy

autor

Roland Coghetto

• Rue de la Brasserie 5, 7100 La Louvière,

Identyfikatory

DOI

10.1515/forma-2016-0009