In this article, we first extend several basic theorems of the operation of vector in 3-dimensional Euclidean spaces. Then three unit vectors: e1, e2, e3 and the definition of vector function in the same spaces are introduced. By dint of unit vector the main operation properties as well as the differentiation formulas of vector function are shown .
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.
In this article, we give some important theorems of forward difference, backward difference, central difference and difference quotient and forward difference, backward difference, central difference and difference quotient formulas of some special functions.
In this article, we give a definition of a functional space which is constructed from all continuous functions defined on a compact topological space. We prove that this functional space is a Banach algebra. Next, we give a definition of a function space which is constructed from all real-valued continuous functions with bounded support. We prove that this function space is a real normed space.
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...
This article introduces the free magma M(X) constructed on a set X . Then, we formalize some theorems about M(X): if f is a function from the set X to a magma N, the free magma M(X) has a unique extension of f to a morphism of M(X) into N and every magma is isomorphic to a magma generated by a set X under a set of relators on M(X). In doing it, the article defines the stable subset under the law...
The aim of this paper is to develop a formal theory of Mizar linguistic concepts following the ideas from  and . The theory presented is an abstraction from the existing implementation of the Mizar system and is devoted to the formalization of Mizar expressions. The concepts formalized here are: standarized constructor signature, arity-rich signatures, and the unification of Mizar expressions.
Financed by the National Centre for Research and Development under grant No. SP/I/1/77065/10 by the strategic scientific research and experimental development program:
SYNAT - “Interdisciplinary System for Interactive Scientific and Scientific-Technical Information”.