The first section consists of auxiliary results about nondecreasing real functions. In the second section a new characterization of relatively compact sets of regulated functions in the sup-norm topology is brought, and the third section includes, among others, an analogue of Helly's Choice Theorem in the space of regulated functions.
This paper deals with regulated functions having values in a Banach space. In particular, families of equiregulated functions are considered and criteria for relative compactness in the space of regulated functions are given.
In this article, the definitions and basic properties of Riemann-Stieltjes integral are formalized in Mizar [1]. In the first section, we showed the preliminary definition. We proved also some properties of finite sequences of real numbers. In Sec. 2, we defined variation. Using the definition, we also defined bounded variation and total variation, and proved theorems about related properties. In Sec. 3, we defined Riemann-Stieltjes integral. Referring to the way of the article [7], we described...