Pełnotekstowe zasoby PLDML oraz innych baz dziedzinowych są już dostępne w nowej Bibliotece Nauki.
Zapraszamy na https://bibliotekanauki.pl
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 12

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last

Wyniki wyszukiwania

help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote

Complex Function Differentiability

100%
Pacharapokin C., Yamazaki H., Shidama Y., Nakamura Y.
Formalized Mathematics
|
2009
|
tom 17
|
nr 2
67-72
EN
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.
2
Content available remote

Morphology for Image Processing. Part I

100%
Yamazaki H., Byliński C., Wasaki K.
Formalized Mathematics
|
2012
|
tom 20
|
nr 1
61-63
EN
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].
3
Content available remote

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

100%
Yamazaki M., Yamazaki H., Shidama Y.
Formalized Mathematics
|
2008
|
tom 16
|
nr 4
311-317
EN
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
4
Content available remote

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

100%
Yamazaki H., Endou N., Shidama Y., Okazaki H.
Formalized Mathematics
|
2007
|
tom 15
|
nr 4
231-235
EN
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.
5
Content available remote

Conservation Rules of Direct Sum Decomposition of Groups

100%
Nakasho K., Yamazaki H., Okazaki H., Shidama Y.
Formalized Mathematics
|
2016
|
tom 24
|
nr 1
81-94
EN
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.
6
Content available remote

The Cauchy-Riemann Differential Equations of Complex Functions

100%
Yamazaki H., Shidama Y., Nakamura Y., Pacharapokin C.
Formalized Mathematics
|
2009
|
tom 17
|
nr 2
147-149
EN
In this article we prove Cauchy-Riemann differential equations of complex functions. These theorems give necessary and sufficient condition for differentiable function.
7
Content available remote

Equivalent Expressions of Direct Sum Decomposition of Groups1

100%
Nakasho K., Okazaki H., Yamazaki H., Shidama Y.
Formalized Mathematics
|
2015
|
tom 23
|
nr 1
67-73
EN
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.
8
Content available remote

Definition and Properties of Direct Sum Decomposition of Groups1

100%
Nakasho K., Yamazaki H., Okazaki H., Shidama Y.
Formalized Mathematics
|
2015
|
tom 23
|
nr 1
15-27
EN
In this article, direct sum decomposition of group is mainly discussed. In the second section, support of element of direct product group is defined and its properties are formalized. It is formalized here that an element of direct product group belongs to its direct sum if and only if support of the element is finite. In the third section, product map and sum map are prepared. In the fourth section, internal and external direct sum are defined. In the last section, an equivalent form of internal direct sum is proved. We referred to [23], [22], [8] and [18] in the formalization.
9
Content available remote

Complex Integral

100%
Yamazaki M., Yamazaki H., Shidama Y., Wasaki K.
Formalized Mathematics
|
2009
|
tom 17
|
nr 4
233-236
EN
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.
10
Content available remote

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

100%
Zhang B., Yamazaki H., Nakamura Y.
Formalized Mathematics
|
2006
|
tom 14
|
nr 4
225-229
EN
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.
11
Content available remote

Isomorphisms of Direct Products of Finite Commutative Groups

100%
Okazaki H., Yamazaki H., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 1
65-74
EN
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
12
Content available remote

Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order

100%
Yamazaki H., Okazaki H., Nakasho K., Shidama Y.
Formalized Mathematics
|
2013
|
tom 21
|
nr 3
207-211
EN
In this paper we formalized some theorems concerning the cyclic groups of prime power order. We formalize that every commutative cyclic group of prime power order is isomorphic to a direct product of family of cyclic groups [1], [18].
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.