# Search Results

## You are looking at 1 - 10 of 12 items for

• Author: Hiroshi Yamazaki
Clear All Modify Search
Open access

## Extended Riemann Integral of Functions of Real Variable and One-sided Laplace Transform

In this article, we defined a variety of extended Riemann integrals and proved that such integration is linear. Furthermore, we defined the one-sided Laplace transform and proved the linearity of that operator.

MML identifier: INTEGR10, version: 7.9.01 4.101.1015

Open access

## Complex Integral

In this article, we defined complex curve and complex integral. Then we have proved the linearity for the complex integral. Furthermore, we have proved complex integral of complex curve's connection is the sum of each complex integral of individual complex curve.

Open access

## Summary

We have been working on the formalization of groups. In [1], we encoded some theorems concerning the product of cyclic groups. In this article, we present the generalized formalization of [1]. First, we show that every finite commutative group which order is composite number is isomorphic to a direct product of finite commutative groups which orders are relatively prime. Next, we describe finite direct products of finite commutative groups

Open access

## Morphology for Image Processing. Part I

In this article we defined mathematical morphology image processing with set operations. First, we defined Minkowski set operations and proved their properties. Next, we defined basic image processing, dilation and erosion proving basic fact about them [5], [8].

Open access

## The Relevance of Measure and Probability, and Definition of Completeness of Probability

In this article, we first discuss the relation between measure defined using extended real numbers and probability defined using real numbers. Further, we define completeness of probability, and its completion method, and also show that they coincide with those of measure.

Open access

## Summary

In this article, conservation rules of the direct sum decomposition of groups are mainly discussed. In the first section, we prepare miscellaneous definitions and theorems for further formalization in Mizar [5]. In the next three sections, we formalized the fact that the property of direct sum decomposition is preserved against the substitutions of the subscript set, flattening of direct sum, and layering of direct sum, respectively. We referred to [14], [13] [6] and [11] in the formalization.

Open access

## Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers

In this article, we extended properties of sequences of real numbers to sequences of extended real numbers. We also introduced basic properties of the inferior limit, superior limit and convergence of sequences of extended real numbers.

Open access

## Summary

In this article, the equivalent expressions of the direct sum decomposition of groups are mainly discussed. In the first section, we formalize the fact that the internal direct sum decomposition can be defined as normal subgroups and some of their properties. In the second section, we formalize an equivalent form of internal direct sum of commutative groups. In the last section, we formalize that the external direct sum leads an internal direct sum. We referred to [19], [18] [8] and [14] in the formalization.

Open access

## Complex Function Differentiability

For a complex valued function defined on its domain in complex numbers the differentiability in a single point and on a subset of the domain is presented. The main elements of differential calculus are developed. The algebraic properties of differential complex functions are shown.

Open access

## The Cauchy-Riemann Differential Equations of Complex Functions

In this article we prove Cauchy-Riemann differential equations of complex functions. These theorems give necessary and sufficient condition for differentiable function.