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: 34

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

Wyniki wyszukiwania

help Sortuj według:

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

Abstract Simplicial Complexes

100%
Pąk K.
Formalized Mathematics
|
2010
|
tom 18
|
nr 1
95-106
EN
In this article we define the notion of abstract simplicial complexes and operations on them. We introduce the following basic notions: simplex, face, vertex, degree, skeleton, subdivision and substructure, and prove some of their properties.
2
Content available remote

Affine Independence in Vector Spaces

100%
Pąk K.
Formalized Mathematics
|
2010
|
tom 18
|
nr 1
87-93
EN
In this article we describe the notion of affinely independent subset of a real linear space. First we prove selected theorems concerning operations on linear combinations. Then we introduce affine independence and prove the equivalence of various definitions of this notion. We also introduce the notion of the affine hull, i.e. a subset generated by a set of vectors which is an intersection of all affine sets including the given set. Finally, we introduce and prove selected properties of the barycentric coordinates.
3
Content available remote

Linear Map of Matrices

100%
Pąk K.
Formalized Mathematics
|
2008
|
tom 16
|
nr 3
269-275
EN
The paper is concerned with a generalization of concepts introduced in [13], i.e. introduced are matrices of linear transformations over a finitedimensional vector space. Introduced are linear transformations over a finitedimensional vector space depending on a given matrix of the transformation. Finally, I prove that the rank of linear transformations over a finite-dimensional vector space is the same as the rank of the matrix of that transformation.
4
Content available remote

The Rotation Group

100%
Pąk K.
Formalized Mathematics
|
2012
|
tom 20
|
nr 1
23-29
EN
We introduce length-preserving linear transformations of Euclidean topological spaces. We also introduce rotation which preserves orientation (proper rotation) and reverses orientation (improper rotation). We show that every rotation that preserves orientation can be represented as a composition of base proper rotations. And finally, we show that every rotation that reverses orientation can be represented as a composition of proper rotations and one improper rotation.
5
Content available remote

Jordan Matrix Decomposition

100%
Pąk K.
Formalized Mathematics
|
2008
|
tom 16
|
nr 4
297-303
EN
In this paper I present the Jordan Matrix Decomposition Theorem which states that an arbitrary square matrix M over an algebraically closed field can be decomposed into the form [...] where S is an invertible matrix and J is a matrix in a Jordan canonical form, i.e. a special type of block diagonal matrix in which each block consists of Jordan blocks (see [13]).MML identifier: MATRIXJ2, version: 7.9.01 4.101.1015
6
Content available remote

Basic Properties of the Rank of Matrices over a Field

100%
Pąk K.
Formalized Mathematics
|
2007
|
tom 15
|
nr 4
199-211
EN
In this paper I present selected properties of triangular matrices and basic properties of the rank of matrices over a field.I define a submatrix as a matrix formed by selecting certain rows and columns from a bigger matrix. That is in my considerations, as an array, it is cut down to those entries constrained by row and column. Then I introduce the concept of the rank of a m x n matrix A by the condition: A has the rank r if and only if, there is a r x r submatrix of A with a non-zero determinant, and for every k x k submatrix of A with a non-zero determinant we have k ≤ r.At the end, I prove that the rank defined by the size of the biggest submatrix with a non-zero determinant of a matrix A, is the same as the maximal number of linearly independent rows of A.
7
Content available remote

Block Diagonal Matrices

100%
Pąk K.
Formalized Mathematics
|
2008
|
tom 16
|
nr 3
259-267
EN
In this paper I present basic properties of block diagonal matrices over a set. In my approach the finite sequence of matrices in a block diagonal matrix is not restricted to square matrices. Moreover, the off-diagonal blocks need not be zero matrices, but also with another arbitrary fixed value.
8
Content available remote

Eigenvalues of a Linear Transformation

100%
Pąk K.
Formalized Mathematics
|
2008
|
tom 16
|
nr 4
289-295
EN
The article presents well known facts about eigenvalues of linear transformation of a vector space (see [13]). I formalize main dependencies between eigenvalues and the diagram of the matrix of a linear transformation over a finite-dimensional vector space. Finally, I formalize the subspace [...] called a generalized eigenspace for the eigenvalue λ and show its basic properties.MML identifier: VECTSP11, version: 7.9.03 4.108.1028
9
Content available remote

The Geometric Interior in Real Linear Spaces

100%
Pąk K.
Formalized Mathematics
|
2010
|
tom 18
|
nr 3
185-188
EN
We introduce the notions of the geometric interior and the centre of mass for subsets of real linear spaces. We prove a number of theorems concerning these notions which are used in the theory of abstract simplicial complexes.
10
Content available remote

Sperner's Lemma

100%
Pąk K.
Formalized Mathematics
|
2010
|
tom 18
|
nr 4
189-196
EN
In this article we introduce and prove properties of simplicial complexes in real linear spaces which are necessary to formulate Sperner's lemma. The lemma states that for a function ƒ, which for an arbitrary vertex υ of the barycentric subdivision B of simplex K assigns some vertex from a face of K which contains υ, we can find a simplex S of B which satisfies ƒ(S) = K (see [10]).
11
Content available remote

Continuity of Barycentric Coordinates in Euclidean Topological Spaces

100%
Pąk K.
Formalized Mathematics
|
2011
|
tom 19
|
nr 3
139-144
EN
In this paper we present selected properties of barycentric coordinates in the Euclidean topological space. We prove the topological correspondence between a subset of an affine closed space of εn and the set of vectors created from barycentric coordinates of points of this subset.
12
Content available remote

Brouwer Fixed Point Theorem for Simplexes

100%
Pąk K.
Formalized Mathematics
|
2011
|
tom 19
|
nr 3
145-150
EN
In this article we prove the Brouwer fixed point theorem for an arbitrary simplex which is the convex hull of its n + 1 affinely indepedent vertices of εn. First we introduce the Lebesgue number, which for an arbitrary open cover of a compact metric space M is a positive real number so that any ball of about such radius must be completely contained in a member of the cover. Then we introduce the notion of a bounded simplicial complex and the diameter of a bounded simplicial complex. We also prove the estimation of diameter decrease which is connected with the barycentric subdivision. Finally, we prove the Brouwer fixed point theorem and compute the small inductive dimension of εn. This article is based on [16].
13
Content available remote

Tietze Extension Theorem for n-dimensional Spaces

100%
Pąk K.
Formalized Mathematics
|
2014
|
tom 22
|
nr 1
11-19
EN
In this article we prove the Tietze extension theorem for an arbitrary convex compact subset of εn with a non-empty interior. This theorem states that, if T is a normal topological space, X is a closed subset of T, and A is a convex compact subset of εn with a non-empty interior, then a continuous function f : X → A can be extended to a continuous function g : T → εn. Additionally we show that a subset A is replaceable by an arbitrary subset of a topological space that is homeomorphic with a convex compact subset of En with a non-empty interior. This article is based on [20]; [23] and [22] can also serve as reference books.
14
Content available remote

Leibniz Series forπ

100%
Pąk K.
Formalized Mathematics
|
2016
|
tom 24
|
nr 4
275-280
EN
In this article we prove the Leibniz series for π which states that π4=∑n=0∞(−1)n2⋅n+1. $${\pi \over 4} = \sum\limits_{n = 0}^\infty {{{\left( { - 1} \right)^n } \over {2 \cdot n + 1}}.} $$ The formalization follows K. Knopp [8], [1] and [6]. Leibniz’s Series for Pi is item #26 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.
15
Content available remote

Topological Manifolds

100%
Pąk K.
Formalized Mathematics
|
2014
|
tom 22
|
nr 2
179-186
EN
Let us recall that a topological space M is a topological manifold if M is second-countable Hausdorff and locally Euclidean, i.e. each point has a neighborhood that is homeomorphic to an open ball of E n for some n. However, if we would like to consider a topological manifold with a boundary, we have to extend this definition. Therefore, we introduce here the concept of a locally Euclidean space that covers both cases (with and without a boundary), i.e. where each point has a neighborhood that is homeomorphic to a closed ball of En for some n. Our purpose is to prove, using the Mizar formalism, a number of properties of such locally Euclidean spaces and use them to demonstrate basic properties of a manifold. Let T be a locally Euclidean space. We prove that every interior point of T has a neighborhood homeomorphic to an open ball and that every boundary point of T has a neighborhood homeomorphic to a closed ball, where additionally this point is transformed into a point of the boundary of this ball. When T is n-dimensional, i.e. each point of T has a neighborhood that is homeomorphic to a closed ball of En, we show that the interior of T is a locally Euclidean space without boundary of dimension n and the boundary of T is a locally Euclidean space without boundary of dimension n − 1. Additionally, we show that every connected component of a compact locally Euclidean space is a locally Euclidean space of some dimension. We prove also that the Cartesian product of locally Euclidean spaces also forms a locally Euclidean space. We determine the interior and boundary of this product and show that its dimension is the sum of the dimensions of its factors. At the end, we present several consequences of these results for topological manifolds. This article is based on [14].
16
Content available remote

Complete Spaces

100%
Pąk K.
Formalized Mathematics
|
2008
|
tom 16
|
nr 1
35-43
EN
This paper is a continuation of [12]. First some definitions needed to formulate Cantor's theorem on complete spaces and show several facts about them are introduced. Next section contains the proof of Cantor's theorem and some properties of complete spaces resulting from this theorem. Moreover, countable compact spaces and proofs of auxiliary facts about them is defined. I also show the important condition that every metric space is compact if and only if it is countably compact. Then I prove that every metric space is compact if and only if it is a complete and totally bounded space. I also introduce the definition of the metric space with the well metric. This article is based on [13].MML identifier: COMPL SP, version: 7.8.05 4.89.993
17
Content available remote

Bertrand’s Ballot Theorem

100%
Pąk K.
Formalized Mathematics
|
2014
|
tom 22
|
nr 2
119-123
EN
In this article we formalize the Bertrand’s Ballot Theorem based on [17]. Suppose that in an election we have two candidates: A that receives n votes and B that receives k votes, and additionally n ≥ k. Then this theorem states that the probability of the situation where A maintains more votes than B throughout the counting of the ballots is equal to (n − k)/(n + k). This theorem is item #30 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.
18
Content available remote

Brouwer Fixed Point Theorem in the General Case

100%
Pąk K.
Formalized Mathematics
|
2011
|
tom 19
|
nr 3
151-153
EN
In this article we prove the Brouwer fixed point theorem for an arbitrary convex compact subset of εn with a non empty interior. This article is based on [15].
19
Content available remote

Brouwer Invariance of Domain Theorem

100%
Pąk K.
Formalized Mathematics
|
2014
|
tom 22
|
nr 1
21-28
EN
In this article we focus on a special case of the Brouwer invariance of domain theorem. Let us A, B be a subsets of εn, and f : A → B be a homeomorphic. We prove that, if A is closed then f transform the boundary of A to the boundary of B; and if B is closed then f transform the interior of A to the interior of B. These two cases are sufficient to prove the topological invariance of dimension, which is used to prove basic properties of the n-dimensional manifolds, and also to prove basic properties of the boundary and the interior of manifolds, e.g. the boundary of an n-dimension manifold with boundary is an (n − 1)-dimension manifold. This article is based on [18]; [21] and [20] can also serve as reference books.
20
Content available remote

The Catalan Numbers. Part II1

100%
Pąk K.
Formalized Mathematics
|
2006
|
tom 14
|
nr 4
153-159
EN
In this paper, we define sequence dominated by 0, in which every initial fragment contains more zeroes than ones. If n ≥ 2 · m and n > 0, then the number of sequences dominated by 0 the length n including m of ones, is given by the formula [...] and satisfies the recurrence relation [...] Obviously, if n = 2 · m, then we obtain the recurrence relation for the Catalan numbers (starting from 0) [...] Using the above recurrence relation we can see that [...] where [...] and hence [...] MML identifier: CATALAN2, version: 7.8.03 4.75.958
first rewind previous Strona / 2 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ć.