author_facet Nakasho, Kazuhisa
Futa, Yuichi
Shidama, Yasunari
Nakasho, Kazuhisa
Futa, Yuichi
Shidama, Yasunari
author Nakasho, Kazuhisa
Futa, Yuichi
Shidama, Yasunari
spellingShingle Nakasho, Kazuhisa
Futa, Yuichi
Shidama, Yasunari
Formalized Mathematics
Continuity of Bounded Linear Operators on Normed Linear Spaces
Applied Mathematics
Computational Mathematics
author_sort nakasho, kazuhisa
spelling Nakasho, Kazuhisa Futa, Yuichi Shidama, Yasunari 1898-9934 1426-2630 Walter de Gruyter GmbH Applied Mathematics Computational Mathematics http://dx.doi.org/10.2478/forma-2018-0021 <jats:title>Summary</jats:title> <jats:p>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 continuous and Lipschitz continuous. Especially, a bounded linear operator on the dense subset of a complete normed linear space has a unique natural extension over the whole space. In the next section, several basic currying properties are formalized.</jats:p> <jats:p>In the last section, we formalized that continuity of bilinear operator is equivalent to both Lipschitz continuity and local continuity. We referred to [4], [13], and [3] in this formalization.</jats:p> Continuity of Bounded Linear Operators on Normed Linear Spaces Formalized Mathematics
doi_str_mv 10.2478/forma-2018-0021
facet_avail Online
Free
finc_class_facet Mathematik
format ElectronicArticle
fullrecord blob:ai-49-aHR0cDovL2R4LmRvaS5vcmcvMTAuMjQ3OC9mb3JtYS0yMDE4LTAwMjE
id ai-49-aHR0cDovL2R4LmRvaS5vcmcvMTAuMjQ3OC9mb3JtYS0yMDE4LTAwMjE
institution DE-Gla1
DE-Zi4
DE-15
DE-Pl11
DE-Rs1
DE-105
DE-14
DE-Ch1
DE-L229
DE-D275
DE-Bn3
DE-Brt1
DE-Zwi2
DE-D161
imprint Walter de Gruyter GmbH, 2018
imprint_str_mv Walter de Gruyter GmbH, 2018
issn 1898-9934
1426-2630
issn_str_mv 1898-9934
1426-2630
language English
mega_collection Walter de Gruyter GmbH (CrossRef)
match_str nakasho2018continuityofboundedlinearoperatorsonnormedlinearspaces
publishDateSort 2018
publisher Walter de Gruyter GmbH
recordtype ai
record_format ai
series Formalized Mathematics
source_id 49
title Continuity of Bounded Linear Operators on Normed Linear Spaces
title_unstemmed Continuity of Bounded Linear Operators on Normed Linear Spaces
title_full Continuity of Bounded Linear Operators on Normed Linear Spaces
title_fullStr Continuity of Bounded Linear Operators on Normed Linear Spaces
title_full_unstemmed Continuity of Bounded Linear Operators on Normed Linear Spaces
title_short Continuity of Bounded Linear Operators on Normed Linear Spaces
title_sort continuity of bounded linear operators on normed linear spaces
topic Applied Mathematics
Computational Mathematics
url http://dx.doi.org/10.2478/forma-2018-0021
publishDate 2018
physical 231-237
description <jats:title>Summary</jats:title> <jats:p>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 continuous and Lipschitz continuous. Especially, a bounded linear operator on the dense subset of a complete normed linear space has a unique natural extension over the whole space. In the next section, several basic currying properties are formalized.</jats:p> <jats:p>In the last section, we formalized that continuity of bilinear operator is equivalent to both Lipschitz continuity and local continuity. We referred to [4], [13], and [3] in this formalization.</jats:p>
container_issue 3
container_start_page 231
container_title Formalized Mathematics
container_volume 26
format_de105 Article, E-Article
format_de14 Article, E-Article
format_de15 Article, E-Article
format_de520 Article, E-Article
format_de540 Article, E-Article
format_dech1 Article, E-Article
format_ded117 Article, E-Article
format_degla1 E-Article
format_del152 Buch
format_del189 Article, E-Article
format_dezi4 Article
format_dezwi2 Article, E-Article
format_finc Article, E-Article
format_nrw Article, E-Article
_version_ 1792330623760728073
geogr_code not assigned
last_indexed 2024-03-01T13:27:52.304Z
geogr_code_person not assigned
openURL url_ver=Z39.88-2004&ctx_ver=Z39.88-2004&ctx_enc=info%3Aofi%2Fenc%3AUTF-8&rfr_id=info%3Asid%2Fvufind.svn.sourceforge.net%3Agenerator&rft.title=Continuity+of+Bounded+Linear+Operators+on+Normed+Linear+Spaces&rft.date=2018-10-01&genre=article&issn=1426-2630&volume=26&issue=3&spage=231&epage=237&pages=231-237&jtitle=Formalized+Mathematics&atitle=Continuity+of+Bounded+Linear+Operators+on+Normed+Linear+Spaces&aulast=Shidama&aufirst=Yasunari&rft_id=info%3Adoi%2F10.2478%2Fforma-2018-0021&rft.language%5B0%5D=eng
SOLR
_version_ 1792330623760728073
author Nakasho, Kazuhisa, Futa, Yuichi, Shidama, Yasunari
author_facet Nakasho, Kazuhisa, Futa, Yuichi, Shidama, Yasunari, Nakasho, Kazuhisa, Futa, Yuichi, Shidama, Yasunari
author_sort nakasho, kazuhisa
container_issue 3
container_start_page 231
container_title Formalized Mathematics
container_volume 26
description <jats:title>Summary</jats:title> <jats:p>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 continuous and Lipschitz continuous. Especially, a bounded linear operator on the dense subset of a complete normed linear space has a unique natural extension over the whole space. In the next section, several basic currying properties are formalized.</jats:p> <jats:p>In the last section, we formalized that continuity of bilinear operator is equivalent to both Lipschitz continuity and local continuity. We referred to [4], [13], and [3] in this formalization.</jats:p>
doi_str_mv 10.2478/forma-2018-0021
facet_avail Online, Free
finc_class_facet Mathematik
format ElectronicArticle
format_de105 Article, E-Article
format_de14 Article, E-Article
format_de15 Article, E-Article
format_de520 Article, E-Article
format_de540 Article, E-Article
format_dech1 Article, E-Article
format_ded117 Article, E-Article
format_degla1 E-Article
format_del152 Buch
format_del189 Article, E-Article
format_dezi4 Article
format_dezwi2 Article, E-Article
format_finc Article, E-Article
format_nrw Article, E-Article
geogr_code not assigned
geogr_code_person not assigned
id ai-49-aHR0cDovL2R4LmRvaS5vcmcvMTAuMjQ3OC9mb3JtYS0yMDE4LTAwMjE
imprint Walter de Gruyter GmbH, 2018
imprint_str_mv Walter de Gruyter GmbH, 2018
institution DE-Gla1, DE-Zi4, DE-15, DE-Pl11, DE-Rs1, DE-105, DE-14, DE-Ch1, DE-L229, DE-D275, DE-Bn3, DE-Brt1, DE-Zwi2, DE-D161
issn 1898-9934, 1426-2630
issn_str_mv 1898-9934, 1426-2630
language English
last_indexed 2024-03-01T13:27:52.304Z
match_str nakasho2018continuityofboundedlinearoperatorsonnormedlinearspaces
mega_collection Walter de Gruyter GmbH (CrossRef)
physical 231-237
publishDate 2018
publishDateSort 2018
publisher Walter de Gruyter GmbH
record_format ai
recordtype ai
series Formalized Mathematics
source_id 49
spelling Nakasho, Kazuhisa Futa, Yuichi Shidama, Yasunari 1898-9934 1426-2630 Walter de Gruyter GmbH Applied Mathematics Computational Mathematics http://dx.doi.org/10.2478/forma-2018-0021 <jats:title>Summary</jats:title> <jats:p>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 continuous and Lipschitz continuous. Especially, a bounded linear operator on the dense subset of a complete normed linear space has a unique natural extension over the whole space. In the next section, several basic currying properties are formalized.</jats:p> <jats:p>In the last section, we formalized that continuity of bilinear operator is equivalent to both Lipschitz continuity and local continuity. We referred to [4], [13], and [3] in this formalization.</jats:p> Continuity of Bounded Linear Operators on Normed Linear Spaces Formalized Mathematics
spellingShingle Nakasho, Kazuhisa, Futa, Yuichi, Shidama, Yasunari, Formalized Mathematics, Continuity of Bounded Linear Operators on Normed Linear Spaces, Applied Mathematics, Computational Mathematics
title Continuity of Bounded Linear Operators on Normed Linear Spaces
title_full Continuity of Bounded Linear Operators on Normed Linear Spaces
title_fullStr Continuity of Bounded Linear Operators on Normed Linear Spaces
title_full_unstemmed Continuity of Bounded Linear Operators on Normed Linear Spaces
title_short Continuity of Bounded Linear Operators on Normed Linear Spaces
title_sort continuity of bounded linear operators on normed linear spaces
title_unstemmed Continuity of Bounded Linear Operators on Normed Linear Spaces
topic Applied Mathematics, Computational Mathematics
url http://dx.doi.org/10.2478/forma-2018-0021