Banach’s Continuous Inverse Theorem and Closed Graph Theorem

In this article we formalize one of the most important theorems of linear operator theory - the Closed Graph Theorem commonly used in a standard text book such as [10] in Chapter 24.3. It states that a surjective closed linear operator between Banach spaces is bounded.

Bibliographic Details
Main Authors: Sakurai Hideki, Okazaki Hiroyuki, Shidama Yasunari
Format: Article
Language:English
Published: Sciendo 2012-12-01
Series:Formalized Mathematics
Online Access:https://doi.org/10.2478/v10037-012-0032-y
id doaj-33a720ebf2ce49ab9675d5dc34c6f267
record_format Article
spelling doaj-33a720ebf2ce49ab9675d5dc34c6f2672021-09-05T18:16:48ZengSciendoFormalized Mathematics1426-26301898-99342012-12-0120427127410.2478/v10037-012-0032-yBanach’s Continuous Inverse Theorem and Closed Graph TheoremSakurai Hideki0Okazaki Hiroyuki1Shidama Yasunari2406-3, Haneo, Naganohara Agatuma, Gunma, JapanShinshu University, Nagano, JapanShinshu University, Nagano, JapanIn this article we formalize one of the most important theorems of linear operator theory - the Closed Graph Theorem commonly used in a standard text book such as [10] in Chapter 24.3. It states that a surjective closed linear operator between Banach spaces is bounded.https://doi.org/10.2478/v10037-012-0032-y
collection DOAJ
language English
format Article
sources DOAJ
author Sakurai Hideki
Okazaki Hiroyuki
Shidama Yasunari
spellingShingle Sakurai Hideki
Okazaki Hiroyuki
Shidama Yasunari
Banach’s Continuous Inverse Theorem and Closed Graph Theorem
Formalized Mathematics
author_facet Sakurai Hideki
Okazaki Hiroyuki
Shidama Yasunari
author_sort Sakurai Hideki
title Banach’s Continuous Inverse Theorem and Closed Graph Theorem
title_short Banach’s Continuous Inverse Theorem and Closed Graph Theorem
title_full Banach’s Continuous Inverse Theorem and Closed Graph Theorem
title_fullStr Banach’s Continuous Inverse Theorem and Closed Graph Theorem
title_full_unstemmed Banach’s Continuous Inverse Theorem and Closed Graph Theorem
title_sort banach’s continuous inverse theorem and closed graph theorem
publisher Sciendo
series Formalized Mathematics
issn 1426-2630
1898-9934
publishDate 2012-12-01
description In this article we formalize one of the most important theorems of linear operator theory - the Closed Graph Theorem commonly used in a standard text book such as [10] in Chapter 24.3. It states that a surjective closed linear operator between Banach spaces is bounded.
url https://doi.org/10.2478/v10037-012-0032-y
work_keys_str_mv AT sakuraihideki banachscontinuousinversetheoremandclosedgraphtheorem
AT okazakihiroyuki banachscontinuousinversetheoremandclosedgraphtheorem
AT shidamayasunari banachscontinuousinversetheoremandclosedgraphtheorem
_version_ 1717786036983037952