Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 4

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote

The Rank+Nullity Theorem

100%
Alama J.
Formalized Mathematics
|
2007
|
tom 15
|
nr 3
137-142
EN
The rank+nullity theorem states that, if T is a linear transformation from a finite-dimensional vector space V to a finite-dimensional vector space W, then dim(V) = rank(T) + nullity(T), where rank(T) = dim(im(T)) and nullity(T) = dim(ker(T)). The proof treated here is standard; see, for example, [14]: take a basis A of ker(T) and extend it to a basis B of V, and then show that dim(im(T)) is equal to |B - A|, and that T is one-to-one on B - A.
2
Content available remote

The Vector Space of Subsets of a Set Based on Symmetric Difference

100%
Alama J.
Formalized Mathematics
|
2008
|
tom 16
|
nr 1
1-5
EN
For each set X, the power set of X forms a vector space over the field Z2 (the two-element field {0, 1} with addition and multiplication done modulo 2): vector addition is disjoint union, and scalar multiplication is defined by the two equations (1 · x:= x, 0 · x := ∅ for subsets x of X). See [10], Exercise 2.K, for more information.MML identifier: BSPACE, version: 7.8.05 4.89.993
3
Content available remote

Euler's Polyhedron Formula

100%
Alama J.
Formalized Mathematics
|
2008
|
tom 16
|
nr 1
7-17
EN
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
4
Content available remote

Tarski Geometry Axioms

51%
Richter W., Grabowski A., Alama J.
Formalized Mathematics
|
2014
|
tom 22
|
nr 2
167-176
EN
This is the translation of the Mizar article containing readable Mizar proofs of some axiomatic geometry theorems formulated by the great Polish mathematician Alfred Tarski [8], and we hope to continue this work. The article is an extension and upgrading of the source code written by the first author with the help of miz3 tool; his primary goal was to use proof checkers to help teach rigorous axiomatic geometry in high school using Hilbert’s axioms. This is largely a Mizar port of Julien Narboux’s Coq pseudo-code [6]. We partially prove the theorem of [7] that Tarski’s (extremely weak!) plane geometry axioms imply Hilbert’s axioms. Specifically, we obtain Gupta’s amazing proof which implies Hilbert’s axiom I1 that two points determine a line. The primary Mizar coding was heavily influenced by [9] on axioms of incidence geometry. The original development was much improved using Mizar adjectives instead of predicates only, and to use this machinery in full extent, we have to construct some models of Tarski geometry. These are listed in the second section, together with appropriate registrations of clusters. Also models of Tarski’s geometry related to real planes were constructed.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.