Zobrazeno 1 - 10
of 209
pro vyhledávání: '"Yasunari Shidama"'
Autor:
Kazuhisa Nakasho, Yasunari Shidama
Publikováno v:
Formalized Mathematics. 30:159-168
Summary Previous Mizar articles [7, 6, 5] formalized the implicit and inverse function theorems for Frechet continuously differentiable maps on Banach spaces. In this paper, using the Mizar system [1], [2], we formalize these theorems on Euclidean sp
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4600ae9d7a71a033943c611ce579e0ef
https://doi.org/10.2478/forma-2022-0012
https://doi.org/10.2478/forma-2022-0012
Publikováno v:
Formalized Mathematics. 29:175-184
Summary In this article, we formalize in Mizar [1], [2] the topological properties of finite-dimensional real normed spaces. In the first section, we formalize the Bolzano-Weierstrass theorem, which states that a bounded sequence of points in an n-di
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::50541b3584901f277e84db94f6c975c3
https://doi.org/10.2478/forma-2021-0017
https://doi.org/10.2478/forma-2021-0017
Publikováno v:
Formalized Mathematics. 29:117-127
Summary. In this paper, we discuss the properties that hold in finite dimensional vector spaces and related spaces. In the Mizar language [1], [2], variables are strictly typed, and their type conversion requires a complicated process. Our purpose is
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::eebe885e7a06cb55b3a48b246e454646
https://doi.org/10.2478/forma-2021-0012
https://doi.org/10.2478/forma-2021-0012
Publikováno v:
Formalized Mathematics, Vol 29, Iss 2, Pp 87-94 (2021)
Summary. In this article we formalize the Ascoli-Arzelà theorem [5], [6], [8] in Mizar [1], [2]. First, we gave definitions of equicontinuousness and equiboundedness of a set of continuous functions [12], [7], [3], [9]. Next, we formalized the Ascol
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::97ca5fc1e2682d6e936cd3c4d24ef9c4
https://doaj.org/article/d100475c6edd46d6bcfef7e6e394ea6d
https://doaj.org/article/d100475c6edd46d6bcfef7e6e394ea6d
Publikováno v:
Formalized Mathematics, Vol 29, Iss 1, Pp 49-62 (2021)
Summary In this article, using the Mizar system [1], [2], first we give a definition of a functional space which is constructed from all continuous functions defined on a compact topological space [5]. We prove that this functional space is a Banach
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ffb60dd1c1d451177c0b8d3ac466ef79
https://doi.org/10.2478/forma-2021-0005
https://doi.org/10.2478/forma-2021-0005
Publikováno v:
Formalized Mathematics, Vol 27, Iss 3, Pp 315-320 (2019)
In this article, we formalize in Mizar a binary operationof points on an elliptic curve overGF(p) in affine coordinates. We show that theoperation is unital, complementable and commutative. Elliptic curve cryptogra-phy, whose security is based on a d
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4ce56ac308e20b26d605a891f302aa4b
https://soar-ir.repo.nii.ac.jp/records/2001208
https://soar-ir.repo.nii.ac.jp/records/2001208
Autor:
Kazuhisa Nakasho, Yasunari Shidama
Publikováno v:
Formalized Mathematics, Vol 27, Iss 2, Pp 117-131 (2019)
Summary In this article, we formalize differentiability of implicit function theorem in the Mizar system [3], [1]. In the first half section, properties of Lipschitz continuous linear operators are discussed. Some norm properties of a direct sum deco
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::603a69b6236146abdb6e51a1b3651255
https://doaj.org/article/8ab128aa71f64594b73d20d977af957f
https://doaj.org/article/8ab128aa71f64594b73d20d977af957f
Autor:
Kazuhisa Nakasho, Yasunari Shidama
Publikováno v:
Formalized Mathematics, Vol 27, Iss 1, Pp 61-65 (2019)
Summary In this article, various definitions of contuity of multilinear operators on normed linear spaces are discussed in the Mizar formalism [4], [1] and [2]. In the first chapter, several basic theorems are prepared to handle the norm of the multi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4bd19017030c7abdb9711b5736561d6e
https://doaj.org/article/764cbd1124734ac7b0a815e3eb69b59e
https://doaj.org/article/764cbd1124734ac7b0a815e3eb69b59e
Publikováno v:
Formalized Mathematics, Vol 26, Iss 3, Pp 231-237 (2018)
Summary In this article, using the Mizar system [1], [2], we discuss the continuity of bounded linear operators on normed linear spaces. In the first section, it is discussed that bounded linear operators on normed linear spaces are uniformly continu
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ed26da0dc545c2f7a503e50f6531fc4d
https://doaj.org/article/cb6133b8a3b54a7a9f1ef4f1b738006f
https://doaj.org/article/cb6133b8a3b54a7a9f1ef4f1b738006f
Publikováno v:
Formalized Mathematics, Vol 25, Iss 4, Pp 269-281 (2017)
Summary In this article, we formalize in Mizar [1], [3] the existence and uniqueness part of the implicit function theorem. In the first section, some composition properties of Lipschitz continuous linear function are discussed. In the second section
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7441fb8ba2e45d82ad12ab02e5b15b1c
https://doi.org/10.1515/forma-2017-0026
https://doi.org/10.1515/forma-2017-0026