Euler's polyhedron theorem states for a polyhedron p, thatV - E + F = 2,where V, E, and F are, respectively, the number of vertices, edges, and faces of p. The formula was first stated in print by Euler in 1758 [11]. The proof given here is based on Poincaré's linear algebraic proof, stated in [17] (with a corrected proof in [18]), as adapted by Imre Lakatos in the latter's Proofs and Refutations [15].As is well known, Euler's formula is not true for all polyhedra. The condition on polyhedra considered here is that of being a homology sphere, which says that the cycles (chains whose boundary is zero) are exactly the bounding chains (chains that are the boundary of a chain of one higher dimension).The present proof actually goes beyond the three-dimensional version of the polyhedral formula given by Lakatos; it is dimension-free, in the sense that it gives a formula in which the dimension of the polyhedron is a parameter. The classical Euler relation V - E + F = 2 is corresponds to the case where the dimension of the polyhedron is 3.The main theorem, expressed in the language of the present article, isSum alternating - characteristic - sequence (p) = 0,where p is a polyhedron. The alternating characteristic sequence of a polyhedron is the sequence [...] where N(k) is the number of polytopes of p of dimension k. The special case of dim(p) = 3 yields Euler's classical relation. (N(-1) and N(3) will turn out to be equal, by definition, to 1.)Two other special cases are proved: the first says that a one-dimensional "polyhedron" that is a homology sphere consists of just two vertices (and thus consists of just a single edge); the second special case asserts that a two-dimensional polyhedron that is a homology sphere (a polygon) has as many vertices as edges.A treatment of the more general version of Euler's relation can be found in [12] and [6]. The former contains a proof of Steinitz's theorem, which shows that the abstract polyhedra treated in Poincaré's proof, which might not appear to be about polyhedra in the usual sense of the word, are in fact embeddable in R3 under certain conditions. It would be valuable to formalize a proof of Steinitz's theorem and relate it to the development contained here.MML identifier: POLYFORM, version: 7.8.05 4.89.993
@article{bwmeta1.element.doi-10_2478_v10037-008-0002-6,
author = {Jesse Alama},
title = {Euler's Polyhedron Formula},
journal = {Formalized Mathematics},
volume = {16},
year = {2008},
pages = {7-17},
zbl = {1294.68132},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_v10037-008-0002-6}
}
Jesse Alama. Euler's Polyhedron Formula. Formalized Mathematics, Tome 16 (2008) pp. 7-17. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_v10037-008-0002-6/
[1] Jesse Alama. The rank+nullity theorem. Formalized Mathematics, 15(3):137-142, 2007.
[2] Jesse Alama. The vector space of subsets of a set based on symmetric difference. Formalized Mathematics, 16(1):1-5, 2008.
[3] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.
[4] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. | Zbl 06213858
[5] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.
[6] Arne Brøndsted. An Introduction to Convex Polytopes. Graduate Texts in Mathematics. Springer, 1983.
[7] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.
[8] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
[9] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
[10] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.
[11] Leonhard Euler. Elementa doctrinae solidorum. Novi Commentarii Academiae Scientarum Petropolitanae, 4:109-140, 1758.
[12] Branko Grünbaum. Convex Polytopes. Number 221 in Graduate Texts in Mathematics. Springer, 2nd edition, 2003.
[13] Eugeniusz Kusak, Wojciech Leończuk, and Michał Muzalewski. Abelian groups, fields and vector spaces. Formalized Mathematics, 1(2):335-342, 1990.
[14] Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887-890, 1990.
[15] Imre Lakatos. Proofs and Refutations: The Logic of Mathematical Discovery. Cambridge University Press, 1976. Edited by John Worrall and Elie Zahar.
[16] Michał Muzalewski. Rings and modules - part II. Formalized Mathematics, 2(4):579-585, 1991.
[17] Henri Poincaré. Sur la généralisation d'un théorème d'Euler relatif aux polyèdres. Comptes Rendus de Séances de l'Academie des Sciences, 117:144, 1893. | Zbl 25.1031.03
[18] Henri Poincaré. Complément à l'analysis situs. Rendiconti del Circolo Matematico di Palermo, 13:285-343, 1899. | Zbl 30.0435.02
[19] Piotr Rudnicki and Andrzej Trybulec. Abian's fixed point theorem. Formalized Mathematics, 6(3):335-338, 1997.
[20] Dariusz Surowik. Cyclic groups and some of their properties - part I. Formalized Mathematics, 2(5):623-627, 1991.
[21] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329-334, 1990.
[22] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501-505, 1990.
[23] Wojciech A. Trybulec. Groups. Formalized Mathematics, 1(5):821-827, 1990.
[24] Wojciech A. Trybulec. Linear combinations in vector space. Formalized Mathematics, 1(5):877-882, 1990.
[25] Wojciech A. Trybulec. Subspaces and cosets of subspaces in vector space. Formalized Mathematics, 1(5):865-870, 1990.
[26] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291-296, 1990.
[27] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
[28] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.
[29] Mariusz Żynel. The Steinitz theorem and the dimension of a vector space. Formalized Mathematics, 5(3):423-428, 1996.