Search Results

You are looking at 1 - 10 of 38 items for

  • Author: Karol Pak x
Clear All Modify Search
Open access

Karol Pąk

Sperner's Lemma

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]).

Open access

Karol Pąk

Continuity of Barycentric Coordinates in Euclidean Topological Spaces

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.

Open access

Karol Pąk

Brouwer Fixed Point Theorem in the General Case

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].

Open access

Karol Pąk

Abstract Simplicial Complexes

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.

Open access

Karol Pąk

Linear Map of Matrices

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.

Open access

Karol Pąk

Small Inductive Dimension of Topological Spaces. Part II

In this paper we present basic properties of n-dimensional topological spaces according to the book [10]. In the article the formalization of Section 1.5 is completed.

Open access

Karol Pąk

The Catalan Numbers. Part II1

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

Open access

Karol Pąk

Summary

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/.

Open access

Karol Pąk

Summary

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].

Open access

Karol Pąk

The Geometric Interior in Real Linear Spaces

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.