Wyniki wyszukiwania

1

Open Mapping Theorem

100%

Sakurai H., Kunimune H., Shidama Y.

Formalized Mathematics

|

2008

|

tom 16

|

nr 4

401-403

EN

In this article we formalize one of the most important theorems of linear operator theory the Open Mapping Theorem commonly used in a standard book such as [8] in chapter 2.4.2. It states that a surjective continuous linear operator between Banach spaces is an open map.MML identifier: LOPBAN 6, version: 7.10.01 4.111.1036

2

Uniform Boundedness Principle

100%

Sakurai H., Kunimune H., Shidama Y.

Formalized Mathematics

|

2008

|

tom 16

|

nr 1

19-21

EN

In this article at first, we proved the lemma of the inferior limit and the superior limit. Next, we proved the Baire category theorem (Banach space version) [20], [9], [3], quoted it and proved the uniform boundedness principle. Moreover, the proof of the Banach-Steinhaus theorem is added.MML identifier: LOPBAN 5, version: 7.8.05 4.89.993

3

Banach’s Continuous Inverse Theorem and Closed Graph Theorem

100%

Sakurai H., Okazaki H., Shidama Y.

Formalized Mathematics

|

2012

|

tom 20

|

nr 4

271-274

EN

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.

Ograniczanie wyników

3 Formalized Mathematics

3 Sakurai H.

3 Shidama Y.

2 Kunimune H.

1 Okazaki H.

1 2012

2 2008

Open Mapping Theorem

Uniform Boundedness Principle

Banach’s Continuous Inverse Theorem and Closed Graph Theorem