http://hdl.handle.net/11320/21343 2026-10-30T08:30:03Z http://hdl.handle.net/11320/21356 Tytuł: Partial Differentiation on Normed Linear Spaces Rⁿ Autorzy: Endou, Noboru; Shidama, Yasunari; Miyajima, Keiichi Abstrakt: In this article, we de ne the partial di erentiation of functions of real variable and prove the linearity of this operator [18]. 2007-01-01T00:00:00Z http://hdl.handle.net/11320/21355 Tytuł: Riemann Indefinite Integral of Functions of Real Variable Autorzy: Shidama, Yasunari; Endou, Noboru; Wasaki, Katsumi Abstrakt: In this article we define the Riemann indefinite integral of functions of real variable and prove the linearity of that [1]. And we give some examples of the indefinite integral of some elementary functions. Furthermore, also the theorem about integral operation and uniform convergent sequence of functions is proved. 2007-01-01T00:00:00Z http://hdl.handle.net/11320/21350 Tytuł: Regular Expression Quantifiers — m to n Occurrences Autorzy: Trybulec, Michał Abstrakt: This article includes proofs of several facts that are supplemental to the theorems proved in [10]. Next, it builds upon that theory to extend the framework for proving facts about formal languages in general and regular expression operators in particular. In this article, two quantifiers are defined and their properties are shown: m to n occurrences (or the union of a range of powers) and optional occurrence. Although optional occurrence is a special case of the previous operator (0 to 1 occurrences), it is often defined in regex applications as a separate operator - hence its explicit definition and properties in the article. Notation and terminology were taken from [13]. 2007-01-01T00:00:00Z http://hdl.handle.net/11320/21347 Tytuł: The Jordan-Hölder Theorem Autorzy: Riccardi, Marco Abstrakt: The goal of this article is to formalize the Jordan-Hölder theorem in the context of group with operators as in the book [5]. Accordingly, the article introduces the structure of group with operators and reformulates some theorems on a group already present in the Mizar Mathematical Library. Next, the article formalizes the Zassenhaus butterfly lemma and the Schreier refinement theorem, and defines the composition series. 2007-01-01T00:00:00Z